# HG changeset patch
# User wenzelm
# Date 855929612 -3600
# Node ID e9e491033b5480418ee8c8979db848ca8bbd434c
# Parent  54f21bf9522ab9eefea4e53d7974a382c86fbead
globally unset ENV, BASH_ENV;

diff -r 54f21bf9522a -r e9e491033b54 lib/scripts/getsettings
--- 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