# HG changeset patch
# User wenzelm
# Date 1375384168 -7200
# Node ID 72bbdc64d0de554420bb763cc43d1db783fa7dda
# Parent  cfa2367d7212b34a863618141ab14a007a457c13
tuned;

diff -r cfa2367d7212 -r 72bbdc64d0de lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Thu Aug 01 20:45:49 2013 +0200
+++ b/lib/scripts/run-polyml	Thu Aug 01 21:09:28 2013 +0200
@@ -2,7 +2,7 @@
 #
 # Author: Makarius
 #
-# Poly/ML 5.1/5.2 startup script.
+# Startup script for Poly/ML 5.1 ... 5.5.
 
 export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
 
@@ -33,13 +33,8 @@
 POLY="$ML_HOME/poly"
 check_file "$POLY"
 
-if [ "$(basename "$ML_HOME")" = bin ]; then
-  POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)"
-else
-  POLYLIB="$ML_HOME"
-fi
+librarypath "$ML_HOME"
 
-librarypath "$POLYLIB"
 
 
 ## prepare databases