Admin/polyml/bin/polyml
author wenzelm
Mon, 05 Feb 2001 21:33:47 +0100
changeset 11074 100637226ff5
parent 11073 e45b136716f5
child 11082 9a7cdfaa7ecb
permissions -rwxr-xr-x
improved;

#!/bin/sh -x
#
# Poly/ML wrapper script


## self references

if [ -h "$0" ]; then
  THIS="`cd "\`dirname "$0"\`"; cd "\`dirname "\\\`find "$PRG" -ls | cut -d ">" -f 2\\\`"\`"; pwd`"
else
  THIS="`cd "\`dirname "$0"\`"; pwd`"
fi

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


## run poly

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