diff options
| author | krasimir <krasimir@chalmers.se> | 2016-02-17 14:52:48 +0000 |
|---|---|---|
| committer | krasimir <krasimir@chalmers.se> | 2016-02-17 14:52:48 +0000 |
| commit | 8548979d1cc6646c159a9a5fe19095aa753c5975 (patch) | |
| tree | 14e28433e2539afac23b28d1c7d1c9ace8d7cafb /src/runtime/java/Makefile | |
| parent | 9e3944951c68dc367bf73e73a40d0c16f4ced0cf (diff) | |
Now we even test in two different places for the JNI headers. Once for Linux and once for Mac OS. This is still not ideal since different Linux distributions might use different locations.
Diffstat (limited to 'src/runtime/java/Makefile')
| -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) |