# HG changeset patch
# User wenzelm
# Date 1459944537 -7200
# Node ID 64f44d7279e599a8e4d61a113934714717683c04
# Parent  6b2c60ebd915ba483ab0f84b02ab778e08669f44
proper return code;

diff -r 6b2c60ebd915 -r 64f44d7279e5 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Wed Apr 06 14:02:12 2016 +0200
+++ b/src/Pure/Tools/ml_process.scala	Wed Apr 06 14:08:57 2016 +0200
@@ -140,7 +140,8 @@
     val more_args = getopts(args)
     if (args.isEmpty || !more_args.isEmpty) getopts.usage()
 
-    ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
+    val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
       result().print_stdout.rc
+    sys.exit(rc)
   })
 }