# HG changeset patch
# User wenzelm
# Date 861725142 -7200
# Node ID 4be22c30096663edb35f2966fb92ca2e7c17e72f
# Parent  38c0b6dbd24f22998c92b235b701e2b7f409e51d
fixed bash-2.0 problem;

diff -r 38c0b6dbd24f -r 4be22c300966 lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Tue Apr 22 11:49:55 1997 +0200
+++ b/lib/scripts/run-smlnj	Tue Apr 22 18:05:42 1997 +0200
@@ -54,7 +54,7 @@
 START_SML="$ML_HOME/sml $ML_OPTIONS $DB"
 
 if [ -n "$TERMINATE" ]; then
-  { echo "$MLTEXT" "$MLEXIT" } | $START_SML
+  echo "$MLTEXT" "$MLEXIT" | $START_SML
   RC=$?
 elif [ -z "$MLTEXT" ]; then
   sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
diff -r 38c0b6dbd24f -r 4be22c300966 lib/scripts/run-smlnj-0.93
--- a/lib/scripts/run-smlnj-0.93	Tue Apr 22 11:49:55 1997 +0200
+++ b/lib/scripts/run-smlnj-0.93	Tue Apr 22 18:05:42 1997 +0200
@@ -50,7 +50,7 @@
 START_SML="$INFILE $ML_OPTIONS"
 
 if [ -n "$TERMINATE" ]; then
-  { echo "$MLTEXT" "$MLEXIT" } | $START_SML
+  echo "$MLTEXT" "$MLEXIT" | $START_SML
   RC=$?
 elif [ -z "$MLTEXT" ]; then
   sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"