changeset 72570 | 79661d12155e |
parent 71713 | 928fd852f3e2 |
child 72627 | 8d83acc5062e |
--- 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))