# HG changeset patch
# User wenzelm
# Date 850145993 -3600
# Node ID c0165f34e98794c5b33f71db2768175cf447c381
# Parent  8e45991e36014064bd6d7a0caa4e5fba88b28725
getplatform - bash source script to augment current env;

diff -r 8e45991e3601 -r c0165f34e987 lib/scripts/getplatform
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/getplatform	Mon Dec 09 16:39:53 1996 +0100
@@ -0,0 +1,10 @@
+#
+# $Id$
+#
+# getplatform - bash source script to augment current env.
+#
+
+#get bash-style platform info
+unset HOSTTYPE
+unset OSTYPE
+PLATFORM=$(bash -norc -c 'echo $HOSTTYPE-$OSTYPE')