# HG changeset patch
# User wenzelm
# Date 1746608417 -7200
# Node ID f22704ac73c3514f7853e9a7068bbdca42dfa07a
# Parent  2757f73abda7d792a7a9ed80f93dbd92bdde6549
tuned;

diff -r 2757f73abda7 -r f22704ac73c3 src/Pure/Admin/component_polyml.scala
--- a/src/Pure/Admin/component_polyml.scala	Wed May 07 10:45:09 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala	Wed May 07 11:00:17 2025 +0200
@@ -46,8 +46,6 @@
   ) {
     def polyml(arch_64: Boolean): String =
       (if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name
-
-    def sha1: String = platform.arch_64 + "-" + platform.os_name
   }
 
 
@@ -160,7 +158,7 @@
     val sha1_files =
       sha1_root match {
         case Some(dir) =>
-          val platform_path = Path.explode(platform_info.sha1)
+          val platform_path = Path.explode(platform.ISABELLE_PLATFORM(windows = true, apple = true))
           val platform_dir = dir + platform_path
           platform_context.execute(dir, "./build " + File.bash_path(platform_path))
           File.read_dir(platform_dir).map(entry => platform_dir + Path.basic(entry))