prefer high-level Other_Isabelle.bash over low-level SSH.execute;
authorwenzelm
Sat, 28 Jan 2023 20:21:55 +0100
changeset 77127 a8f002720ebb
parent 77126 973cd25af280
child 77128 f40c36ab154d
prefer high-level Other_Isabelle.bash over low-level SSH.execute;
src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Jan 28 20:13:40 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Sat Jan 28 20:21:55 2023 +0100
@@ -580,18 +580,14 @@
         val build_options = (if (afp_repos.isEmpty) "" else " -A") + " " + options
         try {
           val script =
-            Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
-              ssh.bash_path(self_isabelle.isabelle_home + Path.explode("Admin/build_other")) +
+            ssh.bash_path(Path.explode("Admin/build_other")) +
               (if (clean_platforms)
                 " -O " + Bash.string(ssh.isabelle_platform.ISABELLE_PLATFORM_FAMILY)
                else "") +
               (if (clean_archives) " -Q" else "") +
               " -o " + ssh.bash_path(output_file) + build_options + " " +
               ssh.bash_path(isabelle_other) + " " + args
-          ssh.execute(script,
-            progress_stdout = progress.echo,
-            progress_stderr = progress.echo,
-            strict = false).check
+          self_isabelle.bash(script, echo = true, strict = false).check
         }
         catch {
           case ERROR(msg) =>