# HG changeset patch
# User wenzelm
# Date 981575800 -3600
# Node ID 9a7cdfaa7ecbe0850f8483b1ca54f190beb7b32e
# Parent  ce9a6746cd1e9a95142fcbf49f52faa3e09018e7
improved;

diff -r ce9a6746cd1e -r 9a7cdfaa7ecb Admin/polyml/bin/polyml
--- a/Admin/polyml/bin/polyml	Wed Feb 07 17:40:56 2001 +0100
+++ b/Admin/polyml/bin/polyml	Wed Feb 07 20:56:40 2001 +0100
@@ -1,12 +1,14 @@
-#!/bin/sh -x
+#!/bin/sh
 #
-# Poly/ML wrapper script
+# platform independent Poly/ML wrapper script
 
 
 ## self references
 
+PRG="`basename "$0"`"
+
 if [ -h "$0" ]; then
-  THIS="`cd "\`dirname "$0"\`"; cd "\`dirname "\\\`find "$PRG" -ls | cut -d ">" -f 2\\\`"\`"; pwd`"
+  THIS="`cd "\`dirname "$0"\`"; cd "\`dirname "\\\`ls -l "$PRG" | sed -e 's/^.* -> //'\\\`"\`"; pwd`"
 else
   THIS="`cd "\`dirname "$0"\`"; pwd`"
 fi