src/Pure/ML/ml_process.scala
changeset 72112 3546dd4ade74
parent 71881 71de0a253842
child 72118 84f716e72fa3
--- a/src/Pure/ML/ml_process.scala	Fri Aug 07 15:13:50 2020 +0200
+++ b/src/Pure/ML/ml_process.scala	Fri Aug 07 20:19:49 2020 +0200
@@ -124,7 +124,7 @@
       val ml_options2 =
         if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1
         else ml_options1 ::: List("--codepage", "utf8")
-      ml_options2
+      ml_options2 ::: List("--exportstats")
     }
 
     // bash