Admin/polyml/bin/polyml
changeset 11082 9a7cdfaa7ecb
parent 11074 100637226ff5
equal deleted inserted replaced
11081:ce9a6746cd1e 11082:9a7cdfaa7ecb
     1 #!/bin/sh -x
     1 #!/bin/sh
     2 #
     2 #
     3 # Poly/ML wrapper script
     3 # platform independent Poly/ML wrapper script
     4 
     4 
     5 
     5 
     6 ## self references
     6 ## self references
     7 
     7 
       
     8 PRG="`basename "$0"`"
       
     9 
     8 if [ -h "$0" ]; then
    10 if [ -h "$0" ]; then
     9   THIS="`cd "\`dirname "$0"\`"; cd "\`dirname "\\\`find "$PRG" -ls | cut -d ">" -f 2\\\`"\`"; pwd`"
    11   THIS="`cd "\`dirname "$0"\`"; cd "\`dirname "\\\`ls -l "$PRG" | sed -e 's/^.* -> //'\\\`"\`"; pwd`"
    10 else
    12 else
    11   THIS="`cd "\`dirname "$0"\`"; pwd`"
    13   THIS="`cd "\`dirname "$0"\`"; pwd`"
    12 fi
    14 fi
    13 
    15 
    14 SUPER="`cd "$THIS/.."; pwd`"
    16 SUPER="`cd "$THIS/.."; pwd`"