# HG changeset patch
# User wenzelm
# Date 849701906 -3600
# Node ID 67bf78c7c725bd53c3c1a090323764154875a5fa
# Parent  d97eef3982570fa1d3be1e1107d027405035b231
replaced cat by ucat;
fixed RC handling;

diff -r d97eef398257 -r 67bf78c7c725 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Wed Dec 04 13:17:50 1996 +0100
+++ b/lib/scripts/run-polyml	Wed Dec 04 13:18:26 1996 +0100
@@ -1,13 +1,11 @@
 #!/bin/bash
 #
+# $Id$
+#
 # Poly/ML startup script.
 #
-# $Id$
-#
 # Global vars: INFILE OUTFILE COPYDB MLTEXT OPTIONS TERMINATE,
 # and from settings
-#
-# MMW 22-Nov-1996, MMW 25-Nov-1996
 
 
 ## diagnostics
@@ -28,15 +26,10 @@
 DISCGARB=$ML_HOME/discgarb
 
 case "$ML_SYSTEM" in
-  polyml-2.07)
-    ;;
   polyml-3.1)
-    DISCGARB="$ML_HOME/discgarb -c"
+    DISCGARB="$DISCGARB -c"
     export LM_LICENSE_FILE=$ML_HOME/license.dat
     ;;
-  *)
-    fail "Unknown ML system: \"$ML_SYSTEM\""
-    ;;
 esac
 
 
@@ -87,11 +80,11 @@
 else
   TMP_FILE=/tmp/mltext-$$
   echo "$MLTEXT" >$TMP_FILE
-  cat $TMP_FILE - | $START_POLY
+  $ISABELLE_HOME/lib/scripts/ucat $TMP_FILE - | $START_POLY
   RC=$?
   rm $TMP_FILE
 fi
 
-[ $RC -a -n "$OUTFILE" ] && $DISCGARB "$OUTFILE"
+[ $RC -eq 0 -a -n "$OUTFILE" ] && $DISCGARB "$OUTFILE"
 
 exit $RC