lib/scripts/getsettings
changeset 48495 bf5b45870110
parent 48455 a509f19d4cc6
child 48551 1f20dfc22000
equal deleted inserted replaced
48494:00eb5be9e76b 48495:bf5b45870110
   209 #enforce JAVA_HOME
   209 #enforce JAVA_HOME
   210 export JAVA_HOME="$ISABELLE_JDK_HOME"
   210 export JAVA_HOME="$ISABELLE_JDK_HOME"
   211 
   211 
   212 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   212 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   213 
   213 
       
   214 #build condition etc.
       
   215 case "$ML_SYSTEM" in
       
   216   polyml*)
       
   217     ISABELLE_POLYML="true"
       
   218     ;;
       
   219   *)
       
   220     ISABELLE_POLYML=""
       
   221     ;;
       
   222 esac
       
   223 
   214 set +o allexport
   224 set +o allexport
   215 
   225 
   216 fi
   226 fi