changeset 68012 | 6d38b4fd872e |
parent 67099 | 3345d53e7c58 |
child 68219 | c0341c0080e2 |
--- 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