# HG changeset patch
# User wenzelm
# Date 1524216852 -7200
# Node ID 6d38b4fd872eb572c9458e7b2e64be1e5802d4f9
# Parent  72e1d5da30c6fcb2859155626bda3b48b6f4c092
more robust, notably for jdk-10.0.1 where jre is absent;

diff -r 72e1d5da30c6 -r 6d38b4fd872e 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