diff options
Diffstat (limited to 'src/runtime/java/Makefile')
| -rw-r--r-- | src/runtime/java/Makefile | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/runtime/java/Makefile b/src/runtime/java/Makefile index 52342ac27..68855274b 100644 --- a/src/runtime/java/Makefile +++ b/src/runtime/java/Makefile @@ -2,16 +2,10 @@ 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 |