lib/scripts/getsettings
changeset 48495 bf5b45870110
parent 48455 a509f19d4cc6
child 48551 1f20dfc22000
     1.1 --- a/lib/scripts/getsettings	Tue Jul 24 23:01:55 2012 +0200
     1.2 +++ b/lib/scripts/getsettings	Wed Jul 25 10:55:02 2012 +0200
     1.3 @@ -211,6 +211,16 @@
     1.4  
     1.5  ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
     1.6  
     1.7 +#build condition etc.
     1.8 +case "$ML_SYSTEM" in
     1.9 +  polyml*)
    1.10 +    ISABELLE_POLYML="true"
    1.11 +    ;;
    1.12 +  *)
    1.13 +    ISABELLE_POLYML=""
    1.14 +    ;;
    1.15 +esac
    1.16 +
    1.17  set +o allexport
    1.18  
    1.19  fi