changeset 62577 | 7e2aa1d67dd8 |
parent 62562 | 905a5db3932d |
child 62586 | a522a5692832 |
--- a/src/Pure/Tools/ml_console.scala Wed Mar 09 20:36:29 2016 +0100 +++ b/src/Pure/Tools/ml_console.scala Wed Mar 09 20:44:02 2016 +0100 @@ -68,7 +68,7 @@ // process loop val process = - ML_Process(options, heap = logic, + ML_Process(options, heap = logic, args = List("-i"), modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII")) val process_output = Future.thread[Unit]("process_output") { try {