# HG changeset patch # User wenzelm # Date 1237488549 -3600 # Node ID a66fe59e0a26cc4fbf87aea4a487d5bf6024b0b5 # Parent 6c9c00ea4ae6e7a2c00e37c5c35a37256fdc4742 RAW: provide dummy Isar.main to make tty work gracefully (with ML toplevel); diff -r 6c9c00ea4ae6 -r a66fe59e0a26 src/Pure/mk --- a/src/Pure/mk Thu Mar 19 18:20:27 2009 +0100 +++ b/src/Pure/mk Thu Mar 19 19:49:09 2009 +0100 @@ -91,6 +91,7 @@ -e "val ml_system = \"$ML_SYSTEM\";" \ -e "val ml_platform = \"$ML_PLATFORM\";" \ -e "use\"$COMPAT\" handle _ => exit 1;" \ + -e "structure Isar = struct fun main () = () end;" \ -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 RC="$?" elif [ -n "$RAW_SESSION" ]; then