# HG changeset patch
# User wenzelm
# Date 1460221751 -7200
# Node ID 09b516854210593bc3955cb52e6fa598d313d1a7
# Parent  51ac6bc389e89739ad7a2cd657a0e1a7ebb22132
flags as in 'ML' command;

diff -r 51ac6bc389e8 -r 09b516854210 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sat Apr 09 16:16:05 2016 +0200
+++ b/src/Pure/ML/ml_context.ML	Sat Apr 09 19:09:11 2016 +0200
@@ -220,4 +220,4 @@
 
 end;
 
-val ML = ML_Context.eval_source ML_Compiler.flags;
+val ML = ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags);