# HG changeset patch
# User wenzelm
# Date 1708075910 -3600
# Node ID 8e97d1fcbbc2524f4ba19d49e66d8430bab40ec5
# Parent  e905fb37467ff5318918f07a43d8b3b7cf162b59
clarified signature;

diff -r e905fb37467f -r 8e97d1fcbbc2 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Fri Feb 16 09:24:45 2024 +0100
+++ b/src/Pure/Build/build.scala	Fri Feb 16 10:31:50 2024 +0100
@@ -585,7 +585,7 @@
     verbose: Boolean = false
   ): String = {
     val options = build_options ::: Options.Spec.eq("build_hostname", host.name) :: host.options
-    ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " build_worker" +
+    ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " build_worker" +
       if_proper(build_id, " -B " + Bash.string(build_id)) +
       if_proper(afp_root, " -A " + ssh.bash_path(afp_root.get)) +
       dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
diff -r e905fb37467f -r 8e97d1fcbbc2 src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Fri Feb 16 09:24:45 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Fri Feb 16 10:31:50 2024 +0100
@@ -18,7 +18,7 @@
     isabelle_home: Path = Path.current,
   ): String = {
     val options = Options.Spec.eq("build_hostname", host.name) :: host.options
-    ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " build_benchmark" +
+    ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " build_benchmark" +
       Options.Spec.bash_strings(options, bg = true)
   }
 
diff -r e905fb37467f -r 8e97d1fcbbc2 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Fri Feb 16 09:24:45 2024 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Fri Feb 16 10:31:50 2024 +0100
@@ -87,6 +87,8 @@
 
   /* command line entry point */
 
+  def exe(isabelle_home: Path): Path = isabelle_home + Path.explode("bin/isabelle")
+
   def main(args: Array[String]): Unit = {
     Command_Line.tool {
       args.toList match {