Admin/polyml/bin/polyml
author wenzelm
Wed, 07 Feb 2001 20:56:40 +0100
changeset 11082 9a7cdfaa7ecb
parent 11074 100637226ff5
permissions -rwxr-xr-x
improved;

#!/bin/sh
#
# platform independent Poly/ML wrapper script


## self references

PRG="`basename "$0"`"

if [ -h "$0" ]; then
  THIS="`cd "\`dirname "$0"\`"; cd "\`dirname "\\\`ls -l "$PRG" | sed -e 's/^.* -> //'\\\`"\`"; pwd`"
else
  THIS="`cd "\`dirname "$0"\`"; pwd`"
fi

SUPER="`cd "$THIS/.."; pwd`"


## run poly

PLATFORM=`"$THIS/polyml-platform"`
exec "$SUPER/$PLATFORM/poly" $*