--- a/lib/scripts/getsettings Fri Feb 14 12:19:42 1997 +0100
+++ b/lib/scripts/getsettings Fri Feb 14 15:13:32 1997 +0100
@@ -9,10 +9,14 @@
set -o allexport
+#users tend to put strange things in here
+unset ENV
+unset BASH_ENV
+
#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')
+PLATFORM=$(bash -norc -c 'echo $HOSTTYPE-$OSTYPE')
. $ISABELLE_HOME/etc/settings || exit 2
[ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings