# HG changeset patch
# User wenzelm
# Date 855929781 -3600
# Node ID 80a81a36dd81d31ded657c61efd851fc34aa2bd1
# Parent  e9e491033b5480418ee8c8979db848ca8bbd434c
semi fix of piping-quit peoblem (should work on systems with *real* sh);

diff -r e9e491033b54 -r 80a81a36dd81 lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Fri Feb 14 15:13:32 1997 +0100
+++ b/lib/scripts/run-smlnj	Fri Feb 14 15:16:21 1997 +0100
@@ -54,10 +54,13 @@
 START_SML="$ML_HOME/sml $ML_OPTIONS $DB"
 
 if [ -n "$TERMINATE" ]; then
-  { echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML
+  { echo "$MLTEXT" "$MLEXIT" } | $START_SML
+  RC=$?
+elif [ -z "$MLTEXT" ]; then
+  sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
   RC=$?
 else
-  { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat; echo "$MLEXIT" } | $START_SML
+  sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
   RC=$?
 fi
 
diff -r e9e491033b54 -r 80a81a36dd81 lib/scripts/run-smlnj-0.93
--- a/lib/scripts/run-smlnj-0.93	Fri Feb 14 15:13:32 1997 +0100
+++ b/lib/scripts/run-smlnj-0.93	Fri Feb 14 15:16:21 1997 +0100
@@ -29,7 +29,7 @@
 MOVE=""
 
 if [ -z "$OUTFILE" ]; then
-  COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);'
+  COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\\n"); false);'
 else
   if [ "$INFILE" -ef "$OUTFILE" ]; then
     OUTDIR=$(dirname "$OUTFILE")/tmp
@@ -50,10 +50,13 @@
 START_SML="$INFILE $ML_OPTIONS"
 
 if [ -n "$TERMINATE" ]; then
-  { echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML
+  { echo "$MLTEXT" "$MLEXIT" } | $START_SML
+  RC=$?
+elif [ -z "$MLTEXT" ]; then
+  sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
   RC=$?
 else
-  { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat; echo "$MLEXIT" } | $START_SML
+  sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
   RC=$?
 fi