tuned;
authorwenzelm
Tue, 18 Oct 2016 16:08:55 +0200
changeset 64305 4bdea66b01b8
parent 64304 96bc94c87a81
child 64306 7b6dc1b36f20
tuned;
src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Oct 18 16:03:30 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Oct 18 16:08:55 2016 +0200
@@ -373,7 +373,7 @@
     options: String = "",
     args: String = ""): List[(String, Bytes)] =
   {
-    val isabelle_admin = ssh.bash_path(isabelle_repos_self + Path.explode("Admin"))
+    val isabelle_admin = isabelle_repos_self + Path.explode("Admin")
 
 
     /* prepare repository clones */
@@ -384,7 +384,7 @@
     if (self_update) {
       isabelle_hg.pull()
       isabelle_hg.update(clean = true)
-      ssh.execute(Bash.string(isabelle_admin + "/build") + " jars_fresh").check
+      ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
     }
 
     Mercurial.setup_repository(
@@ -395,7 +395,7 @@
 
     val result =
       ssh.execute(
-        Bash.string(isabelle_admin + "/build_history") + " " + options + " " +
+        ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
           ssh.bash_path(isabelle_repos_other) + " " + args,
         progress_stderr = progress.echo(_)).check