clarified signature;
authorwenzelm
Fri, 16 Feb 2024 10:31:50 +0100
changeset 79624 8e97d1fcbbc2
parent 79623 e905fb37467f
child 79625 96bfb554b216
clarified signature;
src/Pure/Build/build.scala
src/Pure/Build/build_benchmark.scala
src/Pure/System/isabelle_tool.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 +
--- 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)
   }
 
--- 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 {