author | wenzelm |
Wed, 06 Apr 2016 14:08:57 +0200 | |
changeset 62888 | 64f44d7279e5 |
parent 62887 | 6b2c60ebd915 |
child 62889 | 99c7f31615c2 |
--- 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) }) }