--- a/lib/scripts/getsettings Sat May 19 14:52:01 2018 +0200
+++ b/lib/scripts/getsettings Sat May 19 15:45:45 2018 +0200
@@ -99,8 +99,6 @@
ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
fi
-ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
-
#enforce JAVA_HOME
if [ -d "$ISABELLE_JDK_HOME/jre" ]
then