--- a/src/Pure/ML/ml_process.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/ML/ml_process.scala Wed Jan 15 19:54:50 2020 +0100
@@ -128,8 +128,8 @@
// bash
val bash_args =
ml_runtime_options :::
- (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
- map(eval => List("--eval", eval)).flatten ::: args
+ (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process)
+ .flatMap(eval => List("--eval", eval)) ::: args
Bash.process(
"exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
@@ -180,7 +180,7 @@
"o:" -> (arg => options = options + arg))
val more_args = getopts(args)
- if (args.isEmpty || !more_args.isEmpty) getopts.usage()
+ if (args.isEmpty || more_args.nonEmpty) getopts.usage()
val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
result().print_stdout.rc