# HG changeset patch
# User wenzelm
# Date 1476799735 -7200
# Node ID 4bdea66b01b8d7836bbf061dc404874bcd3a7bf9
# Parent  96bc94c87a81b1607d512e4b94944d7f224c9616
tuned;

diff -r 96bc94c87a81 -r 4bdea66b01b8 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