# HG changeset patch
# User wenzelm
# Date 1482072083 -3600
# Node ID 476e89d0627246417cd9e3c52ba1b116827adedc
# Parent  1c252d8b6ca6ed20d917f480ef82d2ff02f5a6ed
expose stderr, e.g. Multithreading.tracing;

diff -r 1c252d8b6ca6 -r 476e89d06272 src/Pure/Tools/ml_console.scala
--- 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") {