tuned error message;
authorwenzelm
Thu Nov 11 18:55:17 2010 +0100 (2010-11-11)
changeset 40480d695d258dfbc
parent 40479 cc06f5528bb1
child 40481 da2c56aaaa68
tuned error message;
lib/scripts/run-polyml
     1.1 --- a/lib/scripts/run-polyml	Thu Nov 11 17:07:05 2010 +0100
     1.2 +++ b/lib/scripts/run-polyml	Thu Nov 11 18:55:17 2010 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4    EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
     1.5  else
     1.6    check_file "$INFILE"
     1.7 -  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \"\\n\"); OS.Process.exit OS.Process.failure));"
     1.8 +  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.failure));"
     1.9    EXIT=""
    1.10  fi
    1.11  
    1.12 @@ -78,3 +78,5 @@
    1.13  [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    1.14  
    1.15  exit "$RC"
    1.16 +
    1.17 +#:wrap=soft:maxLineLen=100: