# HG changeset patch
# User wenzelm
# Date 1674933715 -3600
# Node ID a8f002720ebb5a8120b652c9e47cb11fc437ddbc
# Parent  973cd25af2803dd7a3022d28beaed31faaeb501f
prefer high-level Other_Isabelle.bash over low-level SSH.execute;

diff -r 973cd25af280 -r a8f002720ebb 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) =>