diff options
| author | krasimir <krasimir@chalmers.se> | 2017-01-24 09:36:39 +0000 |
|---|---|---|
| committer | krasimir <krasimir@chalmers.se> | 2017-01-24 09:36:39 +0000 |
| commit | f6ecf0ce56a64869fb142aa78bd969efd0f60a5c (patch) | |
| tree | cce1e4b2a3210c1d1f5ddd64aa953b286a2d26a1 /src/runtime/java/Makefile | |
| parent | 1dbba8f37748eeb215809c32c13b61e12959b116 (diff) | |
resolve a conflict that was for some reason commited in src/runtime/java/Makefile
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 |
