lib/scripts/getsettings
changeset 62354 fdd6989cc8a0
parent 61319 d84b4d39bce1
child 62412 ffdc5cf36dc5
--- 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