# HG changeset patch
# User wenzelm
# Date 1495532855 -7200
# Node ID 5bc7e080b18221586098e3ecfb079fa2e48f5feb
# Parent  4940682a2e1aff99f8bbf07a8836c1fb1ac31664
clarified build.out progress;

diff -r 4940682a2e1a -r 5bc7e080b182 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue May 23 11:25:20 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue May 23 11:47:35 2017 +0200
@@ -205,9 +205,9 @@
       val build_args1 = List("-v", "-j" + processes) ::: build_args
       val build_result =
       {
-        val progress1 = new Seq_Progress(progress, new File_Progress(build_out))
-        val other_isabelle1 = new Other_Isabelle(progress1, hg.root, isabelle_identifier)
-        other_isabelle1("build " + Bash.strings(build_args1), redirect = true, echo = verbose)
+        val other_isabelle1 =
+          new Other_Isabelle(new File_Progress(build_out), hg.root, isabelle_identifier)
+        other_isabelle1("build " + Bash.strings(build_args1), redirect = true, echo = true)
       }
       val build_end = Date.now()
 
diff -r 4940682a2e1a -r 5bc7e080b182 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Tue May 23 11:25:20 2017 +0200
+++ b/src/Pure/System/progress.scala	Tue May 23 11:47:35 2017 +0200
@@ -65,18 +65,3 @@
 
   override def toString: String = path.toString
 }
-
-class Seq_Progress(progress1: Progress, progress2: Progress) extends Progress
-{
-  override def echo(msg: String)
-  {
-    progress1.echo(msg)
-    progress2.echo(msg)
-  }
-
-  override def theory(session: String, theory: String)
-  {
-    progress1.theory(session, theory)
-    progress2.theory(session, theory)
-  }
-}