Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned startup;
authorwenzelm
Mon, 10 Feb 1997 16:16:55 +0100
changeset 2605 1effe7413486
parent 2604 605e54988d50
child 2606 27cdd600a3b1
tuned startup; semi fix of piping-quit peoblem (should work on systems with *real& sh);
lib/scripts/run-polyml file | annotate | diff | comparison | revisions 
--- a/lib/scripts/run-polyml	Mon Feb 10 15:45:31 1997 +0100
+++ b/lib/scripts/run-polyml	Mon Feb 10 16:16:55 1997 +0100
@@ -67,12 +67,15 @@
 if [ -n "$TERMINATE" ]; then
   echo "$MLTEXT" | $START_POLY
   RC=$?
+elif [ -z "$MLTEXT" ]; then
+  sh -c "$ISABELLE_HOME/lib/Tools/symbolinput | $START_POLY"
+  RC=$?
 else
-  { echo "$MLTEXT"; $ISABELLE_HOME/lib/Tools/symbolinput } | $START_POLY
+  sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/Tools/symbolinput; } | $START_POLY"
   RC=$?
 fi
 
 NEW_DB_INFO=$(ls -l "$DB")
-[ $RC -eq 0 -a -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
+[ -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
 
 exit $RC
isabelle