| changeset 2346 | c0165f34e987 |
| child 2561 | 8ef656dbf4fa |
--- /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')