| 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