diff -r 92050155593e -r c0341c0080e2 lib/scripts/getsettings
--- 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