diff options
| author | krangelov <kr.angelov@gmail.com> | 2019-03-19 11:21:39 +0100 |
|---|---|---|
| committer | krangelov <kr.angelov@gmail.com> | 2019-03-19 11:21:39 +0100 |
| commit | f3d7d55752b5edce489f6f31c6001bc1c754150e (patch) | |
| tree | 7331dc1b963dcd3a8392d9937be987b2b67919ad /src/runtime | |
| parent | 52f2739da1c583b7ded38b859388bc067b9485ee (diff) | |
added one more possible location for Java headers
Diffstat (limited to 'src/runtime')
| -rw-r--r-- | src/runtime/java/Makefile | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/runtime/java/Makefile b/src/runtime/java/Makefile index d5a25a2f6..14f350ea4 100644 --- a/src/runtime/java/Makefile +++ b/src/runtime/java/Makefile @@ -3,9 +3,10 @@ JAVA_SOURCES = $(wildcard org/grammaticalframework/pgf/*.java) \ $(wildcard org/grammaticalframework/sg/*.java) JNI_INCLUDES = $(if $(wildcard /usr/lib/jvm/default-java/include/.*), -I/usr/lib/jvm/default-java/include -I/usr/lib/jvm/default-java/include/linux, \ - $(if $(wildcard /System/Library/Frameworks/JavaVM.framework/Versions/A/Headers/.*), -I/System/Library/Frameworks/JavaVM.framework/Versions/A/Headers, \ - $(if $(wildcard /Library/Java/Home/include/.*), -I/Library/Java/Home/include/ -I/Library/Java/Home/include/darwin, \ - $(error No JNI headers found)))) + $(if $(wildcard /usr/lib/jvm/java-1.11.0-openjdk-amd64/include/.*), -I/usr/lib/jvm/java-1.11.0-openjdk-amd64/include/ -I/usr/lib/jvm/java-1.11.0-openjdk-amd64/include/linux, \ + $(if $(wildcard /System/Library/Frameworks/JavaVM.framework/Versions/A/Headers/.*), -I/System/Library/Frameworks/JavaVM.framework/Versions/A/Headers, \ + $(if $(wildcard /Library/Java/Home/include/.*), -I/Library/Java/Home/include/ -I/Library/Java/Home/include/darwin, \ + $(error No JNI headers found))))) # For Windows replace the previous line with something like this: # |