expose stderr, e.g. Multithreading.tracing;
--- a/src/Pure/Tools/ml_console.scala Sun Dec 18 13:46:57 2016 +0100
+++ b/src/Pure/Tools/ml_console.scala Sun Dec 18 15:41:23 2016 +0100
@@ -70,7 +70,7 @@
// process loop
val process =
- ML_Process(options, logic = logic, args = List("-i"), dirs = dirs,
+ ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
raw_ml_system = raw_ml_system, store = Sessions.store(system_mode))
val process_output = Future.thread[Unit]("process_output") {