fixed problems with strange user .bashrc etc. (stty, ...);
--- 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')