flags as in 'ML' command;
authorwenzelm
Sat Apr 09 19:09:11 2016 +0200 (2016-04-09)
changeset 6293109b516854210
parent 62930 51ac6bc389e8
child 62932 db12de2367ca
flags as in 'ML' command;
src/Pure/ML/ml_context.ML
     1.1 --- a/src/Pure/ML/ml_context.ML	Sat Apr 09 16:16:05 2016 +0200
     1.2 +++ b/src/Pure/ML/ml_context.ML	Sat Apr 09 19:09:11 2016 +0200
     1.3 @@ -220,4 +220,4 @@
     1.4  
     1.5  end;
     1.6  
     1.7 -val ML = ML_Context.eval_source ML_Compiler.flags;
     1.8 +val ML = ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags);