--- a/lib/scripts/getsettings Thu Feb 06 18:22:59 1997 +0100
+++ b/lib/scripts/getsettings Thu Feb 06 18:27:47 1997 +0100
@@ -9,10 +9,16 @@
set -o allexport
+#get bash-style platform info -- has to work around some tricky features
+unset HOSTTYPE
+unset OSTYPE
+PLATFORM=$(unset ENV; unset BASH_ENV; bash -norc -c 'echo $HOSTTYPE-$OSTYPE')
+
. $ISABELLE_HOME/etc/settings || exit 2
[ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
ISABELLE=$ISABELLE_HOME/bin/isabelle
ISATOOL=$ISABELLE_HOME/bin/isatool
+ISABELLE_OUTPUT_DIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM"
set +o allexport