# HG changeset patch
# User wenzelm
# Date 1398250557 -7200
# Node ID f42717b5dc84301a339a71ea0d36b67605cc9466
# Parent  56335a8e2e8bdf53b24d74f4fb45ad88f6fcb2c3
clarified message and return code, in accordance to ML version;

diff -r 56335a8e2e8b -r f42717b5dc84 src/Pure/System/command_line.scala
--- a/src/Pure/System/command_line.scala	Wed Apr 23 12:51:55 2014 +0200
+++ b/src/Pure/System/command_line.scala	Wed Apr 23 12:55:57 2014 +0200
@@ -30,8 +30,8 @@
       catch {
         case exn: Throwable =>
           if (debug) exn.printStackTrace
-          System.err.println(Exn.message(exn))
-          2
+          System.err.println(cat_lines(split_lines(Exn.message(exn)).map("*** " + _)))
+          Exn.return_code(exn, 2)
       }
     sys.exit(rc)
   }