diff options
Diffstat (limited to 'src/runtime')
| -rw-r--r-- | src/runtime/java/Makefile | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/runtime/java/Makefile b/src/runtime/java/Makefile index 6bf0d1495..52342ac27 100644 --- a/src/runtime/java/Makefile +++ b/src/runtime/java/Makefile @@ -2,10 +2,18 @@ C_SOURCES = jpgf.c jsg.c jni_utils.c JAVA_SOURCES = $(wildcard org/grammaticalframework/pgf/*.java) \ $(wildcard org/grammaticalframework/sg/*.java) +v v v v v v v +JNI_PATH = /usr/lib/jvm/default-java/include +============= +#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 = glibtool --tag=CC LIBTOOL = $(if $(shell command -v glibtool 2>/dev/null), glibtool --tag=CC, libtool) |