equal
deleted
inserted
replaced
52 ## run it! |
52 ## run it! |
53 |
53 |
54 START_SML="$ML_HOME/sml $ML_OPTIONS $DB" |
54 START_SML="$ML_HOME/sml $ML_OPTIONS $DB" |
55 |
55 |
56 if [ -n "$TERMINATE" ]; then |
56 if [ -n "$TERMINATE" ]; then |
57 { echo "$MLTEXT" "$MLEXIT" } | $START_SML |
57 echo "$MLTEXT" "$MLEXIT" | $START_SML |
58 RC=$? |
58 RC=$? |
59 elif [ -z "$MLTEXT" ]; then |
59 elif [ -z "$MLTEXT" ]; then |
60 sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" |
60 sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" |
61 RC=$? |
61 RC=$? |
62 else |
62 else |