# HG changeset patch
# User wenzelm
# Date 1749933348 -7200
# Node ID a71d0beff950fef0db8bfd2129d95db97f4cda3c
# Parent  08dec4389293acb59f859effd5c68d66bdfe6861
proper support for old versions before 0e41f26a0250;

diff -r 08dec4389293 -r a71d0beff950 src/Pure/System/other_isabelle.scala
--- a/src/Pure/System/other_isabelle.scala	Sat Jun 14 22:20:57 2025 +0200
+++ b/src/Pure/System/other_isabelle.scala	Sat Jun 14 22:35:48 2025 +0200
@@ -81,17 +81,19 @@
   def bash_path(path: Path): String = Bash.string(expand_path(path).implode)
 
   def ml_system: String = getenv_strict("ML_SYSTEM")
-  def ml_platform: String = {
-    val Pattern = """.*val ML_PLATFORM = "(.*)".*""".r
-    val input = """val ML_PLATFORM = Option.getOpt (OS.Process.getEnv "ML_PLATFORM", "")"""
-    val result = bash("bin/isabelle console -r", input = input)
-    result.out match {
-      case Pattern(a) if result.ok => a
-      case _ =>
-        error("Cannot get ML_PLATFORM from other Isabelle: " + isabelle_home +
-          if_proper(result.err, "\n" + result.err))
+  def ml_platform: String =
+    if ((isabelle_home + Path.explode("lib/Tools/console")).is_file) {
+      val Pattern = """.*val ML_PLATFORM = "(.*)".*""".r
+      val input = """val ML_PLATFORM = Option.getOpt (OS.Process.getEnv "ML_PLATFORM", "")"""
+      val result = bash("bin/isabelle console -r", input = input)
+      result.out match {
+        case Pattern(a) if result.ok => a
+        case _ =>
+          error("Cannot get ML_PLATFORM from other Isabelle: " + isabelle_home +
+            if_proper(result.err, "\n" + result.err))
+      }
     }
-  }
+    else getenv("ML_PLATFORM")
   def ml_identifier: String = ml_system + "_" + ml_platform
 
   val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER"))