# HG changeset patch
# User wenzelm
# Date 855250067 -3600
# Node ID 363b2c37a1b928f273ee88c37de203e57d5bd9af
# Parent  9d910f3681d020638b1c554a63f2d8dd0943286a
integrated getplatform stuff;
added ISABELLE_OUTPUT_DIR;

diff -r 9d910f3681d0 -r 363b2c37a1b9 lib/scripts/getsettings
--- 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