# HG changeset patch
# User wenzelm
# Date 1708201103 -3600
# Node ID 59debf50c9f7a5eb52c3d4ff0e87270c50fc353b
# Parent  7cfda5c45c79507c27e6c09dc8f3467bffb33897
tuned names;

diff -r 7cfda5c45c79 -r 59debf50c9f7 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sat Feb 17 21:13:10 2024 +0100
+++ b/src/Pure/ML/ml_process.scala	Sat Feb 17 21:18:23 2024 +0100
@@ -98,12 +98,12 @@
     val isabelle_tmp = Isabelle_System.tmp_dir("process")
 
     val ml_runtime_options = {
-      val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
+      val ml_options0 = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
       val ml_options1 =
-        if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
-        else ml_options ::: List("--gcthreads", options.int("threads").toString)
+        if (ml_options0.exists(_.containsSlice("gcthreads"))) ml_options0
+        else ml_options0 ::: List("--gcthreads", options.int("threads").toString)
       val ml_options2 =
-        if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1
+        if (!Platform.is_windows || ml_options0.exists(_.containsSlice("codepage"))) ml_options1
         else ml_options1 ::: List("--codepage", "utf8")
       ml_options2 ::: List("--exportstats")
     }