diff -r a594429637fd -r fdd6989cc8a0 lib/scripts/getsettings --- a/lib/scripts/getsettings Wed Feb 17 21:08:18 2016 +0100 +++ b/lib/scripts/getsettings Wed Feb 17 23:06:24 2016 +0100 @@ -290,16 +290,6 @@ #enforce JAVA_HOME export JAVA_HOME="$ISABELLE_JDK_HOME/jre" -#build condition etc. -case "$ML_SYSTEM" in - polyml*) - ML_SYSTEM_POLYML="true" - ;; - *) - ML_SYSTEM_POLYML="" - ;; -esac - set +o allexport fi