more robust, notably for jdk-10.0.1 where jre is absent;
authorwenzelm
Fri, 20 Apr 2018 11:34:12 +0200
changeset 68012 6d38b4fd872e
parent 68009 72e1d5da30c6
child 68013 7a30a3cc2763
more robust, notably for jdk-10.0.1 where jre is absent;
lib/scripts/getsettings
--- a/lib/scripts/getsettings	Thu Apr 19 21:54:46 2018 +0200
+++ b/lib/scripts/getsettings	Fri Apr 20 11:34:12 2018 +0200
@@ -102,7 +102,12 @@
 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
 
 #enforce JAVA_HOME
-export JAVA_HOME="$ISABELLE_JDK_HOME/jre"
+if [ -d "$ISABELLE_JDK_HOME/jre" ]
+then
+  export JAVA_HOME="$ISABELLE_JDK_HOME/jre"
+else
+  export JAVA_HOME="$ISABELLE_JDK_HOME"
+fi
 
 set +o allexport