# HG changeset patch
# User wenzelm
# Date 1476538931 -7200
# Node ID d78d46c755f811d3a88437abec0c14a2c88275bc
# Parent  3ed43cfc8b14f7a87c827a4818b7e2297e1b4d42
tuned;

diff -r 3ed43cfc8b14 -r d78d46c755f8 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Oct 15 15:23:06 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Oct 15 15:42:11 2016 +0200
@@ -328,16 +328,16 @@
 
 
 
-  /** build_history_remote **/
+  /** remote build_history -- via command-line **/
 
   sealed case class File_Content(name: String, content: Bytes)
 
-  def build_history_remote(
+  def remote_build_history(
     ssh_session: SSH.Session,
     isabelle_repos: Path,
     isabelle_repos_build_history: Path,
-    build_history_options: List[String],
-    build_history_args: List[String],
+    options: String,
+    args: String,
     progress: Progress = Ignore_Progress,
     isabelle_repos_source: String = "http://isabelle.in.tum.de/repos/isabelle",
     self_update: Boolean = false): List[File_Content] =
@@ -367,14 +367,12 @@
           Mercurial.clone_repository(isabelle_repos.implode, isabelle_repos_build_history, ssh = ssh)
 
 
-        /* build_history */
+        /* Admin/build_history */
 
         val result =
           ssh_session.execute(
-            File.bash_string(isabelle_admin + "/build_history") + " " +
-              File.bash_args(build_history_options) + " " +
-              File.bash_path(isabelle_repos_build_history) + " " +
-              File.bash_args(build_history_args),
+            File.bash_string(isabelle_admin + "/build_history") + " " + options + " " +
+              File.bash_path(isabelle_repos_build_history) + " " + args,
             progress_stderr = progress.echo(_))
 
         result.check.out_lines.map(name =>