diff options
Diffstat (limited to 'src/runtime/java')
| -rw-r--r-- | src/runtime/java/Makefile | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/runtime/java/Makefile b/src/runtime/java/Makefile index ce185e044..8310a5720 100644 --- a/src/runtime/java/Makefile +++ b/src/runtime/java/Makefile @@ -2,8 +2,9 @@ C_SOURCES = jpgf.c jsg.c jni_utils.c JAVA_SOURCES = $(wildcard org/grammaticalframework/pgf/*.java) \ $(wildcard org/grammaticalframework/sg/*.java) -JNI_PATH = /usr/lib/jvm/default-java/include -#JNI_PATH = /System/Library/Frameworks/JavaVM.framework/Versions/A/Headers/ +JNI_PATH = $(if $(wildcard /usr/lib/jvm/default-java/include/.*), /usr/lib/jvm/default-java/include, \ + $(if $(wildcard /System/Library/Frameworks/JavaVM.framework/Versions/A/Headers/.*), /System/Library/Frameworks/JavaVM.framework/Versions/A/Headers, \ + $(error No JNI headers found))) INSTALL_PATH = /usr/local/lib LIBTOOL = $(if $(shell command -v glibtool 2>/dev/null), glibtool --tag=CC, libtool) |