# HG changeset patch # User wenzelm # Date 923926804 -7200 # Node ID b2f2770ef8d9e8f5c690acdde4b61d57c91a64ef # Parent 9309bc455432f7077468a9c13b74e431a95411f2 ML_PLATFORM; diff -r 9309bc455432 -r b2f2770ef8d9 NEWS --- a/NEWS Mon Apr 12 15:52:48 1999 +0200 +++ b/NEWS Mon Apr 12 16:20:04 1999 +0200 @@ -45,6 +45,8 @@ * new flag show_tags controls display of tags of theorems (which are basically just comments that may be attached by some tools); +* added ML_PLATFORM setting (useful for cross-platform installations); + *** HOL *** diff -r 9309bc455432 -r b2f2770ef8d9 etc/settings --- a/etc/settings Mon Apr 12 15:52:48 1999 +0200 +++ b/etc/settings Mon Apr 12 16:20:04 1999 +0200 @@ -15,27 +15,32 @@ #ML_SYSTEM=smlnj-110 #ML_HOME=/usr/local/smlnj-110/bin #ML_OPTIONS="@SMLdebug=/dev/null" +#ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys); echo $HEAP_SUFFIX) # MLWorks 2.0 or later #ML_SYSTEM=mlworks #ML_HOME=/usr/local/mlworks/bin #ML_OPTIONS="" +#ML_PLATFORM="" # Poly/ML 2.x #ML_SYSTEM=polyml-2.07 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2 #ML_OPTIONS="-h 30000" +#ML_PLATFORM="" # Poly/ML 3.1 ML_SYSTEM=polyml-3.1 ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4 ML_OPTIONS="-h 30000" +ML_PLATFORM="" LM_LICENSE_FILE=$ML_HOME/license.dat # Standard ML of New Jersey 0.93 #ML_SYSTEM=smlnj-0.93 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src #ML_OPTIONS="" +#ML_PLATFORM="" ### diff -r 9309bc455432 -r b2f2770ef8d9 lib/scripts/getsettings --- a/lib/scripts/getsettings Mon Apr 12 15:52:48 1999 +0200 +++ b/lib/scripts/getsettings Mon Apr 12 16:20:04 1999 +0200 @@ -21,9 +21,14 @@ . $ISABELLE_HOME/etc/settings || exit 2 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings -#append ML system to paths -ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_SYSTEM" -ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_SYSTEM; done) +#append ML system identifier to paths +if [ -z "$ML_PLATFORM" ]; then + ML_IDENTIFIER="$ML_SYSTEM" +else + ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" +fi +ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" +ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_IDENTIFIER; done) ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :) set +o allexport