--- a/lib/scripts/getsettings Wed Apr 16 18:53:36 1997 +0200
+++ b/lib/scripts/getsettings Thu Apr 17 10:30:57 1997 +0200
@@ -15,11 +15,6 @@
unset ENV
unset BASH_ENV
-#get bash-style platform info -- has to work around some tricky features
-unset HOSTTYPE
-unset OSTYPE
-PLATFORM=$(bash -norc -c 'echo $HOSTTYPE-$OSTYPE')
-
#get actual settings
. $ISABELLE_HOME/etc/settings || exit 2
[ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
@@ -27,6 +22,5 @@
#derived values
ISABELLE=$ISABELLE_HOME/bin/isabelle
ISATOOL=$ISABELLE_HOME/bin/isatool
-ISABELLE_OUTPUT_DIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM"
set +o allexport