author | wenzelm |
Tue, 10 Nov 2020 12:45:20 +0100 | |
changeset 72570 | 79661d12155e |
parent 72565 | ed5b907bbf50 |
child 72571 | ab4a0b19648a |
--- a/src/Pure/ML/ml_console.scala Sun Nov 08 21:27:08 2020 +0100 +++ b/src/Pure/ML/ml_console.scala Tue Nov 10 12:45:20 2020 +0100 @@ -42,7 +42,7 @@ "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), - "n" -> (arg => no_build = true), + "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), "r" -> (_ => raw_ml_system = true))