# HG changeset patch
# User wenzelm
# Date 854464875 -3600
# Node ID 8ef656dbf4fa51b1906910dfff9ccf9f4e804e14
# Parent  c57b585eecd90444a80ada237073eaf505f08c27
fixed problems with strange user .bashrc etc. (stty, ...);

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')