changeset 48495 | bf5b45870110 |
parent 48455 | a509f19d4cc6 |
child 48551 | 1f20dfc22000 |
--- a/lib/scripts/getsettings Tue Jul 24 23:01:55 2012 +0200 +++ b/lib/scripts/getsettings Wed Jul 25 10:55:02 2012 +0200 @@ -211,6 +211,16 @@ ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" +#build condition etc. +case "$ML_SYSTEM" in + polyml*) + ISABELLE_POLYML="true" + ;; + *) + ISABELLE_POLYML="" + ;; +esac + set +o allexport fi