functionality added to getsettings;

--- a/lib/scripts/getplatform	Thu Feb 06 18:40:23 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-#
-# $Id$
-#
-# getplatform - bash source script to augment current 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')