--- 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"
--- 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"