lib/scripts/getsettings
changeset 62354 fdd6989cc8a0
parent 61319 d84b4d39bce1
child 62412 ffdc5cf36dc5
     1.1 --- a/lib/scripts/getsettings	Wed Feb 17 21:08:18 2016 +0100
     1.2 +++ b/lib/scripts/getsettings	Wed Feb 17 23:06:24 2016 +0100
     1.3 @@ -290,16 +290,6 @@
     1.4  #enforce JAVA_HOME
     1.5  export JAVA_HOME="$ISABELLE_JDK_HOME/jre"
     1.6  
     1.7 -#build condition etc.
     1.8 -case "$ML_SYSTEM" in
     1.9 -  polyml*)
    1.10 -    ML_SYSTEM_POLYML="true"
    1.11 -    ;;
    1.12 -  *)
    1.13 -    ML_SYSTEM_POLYML=""
    1.14 -    ;;
    1.15 -esac
    1.16 -
    1.17  set +o allexport
    1.18  
    1.19  fi