diff -r c57b585eecd9 -r 8ef656dbf4fa lib/scripts/getplatform
--- a/lib/scripts/getplatform	Mon Jan 27 15:29:39 1997 +0100
+++ b/lib/scripts/getplatform	Tue Jan 28 16:21:15 1997 +0100
@@ -4,7 +4,7 @@
 # getplatform - bash source script to augment current env.
 #
 
-#get bash-style platform info
+#get bash-style platform info -- has to work around some tricky features
 unset HOSTTYPE
 unset OSTYPE
-PLATFORM=$(bash -norc -c 'echo $HOSTTYPE-$OSTYPE')
+PLATFORM=$(unset ENV; unset BASH_ENV; bash -norc -c 'echo $HOSTTYPE-$OSTYPE')