# HG changeset patch
# User wenzelm
# Date 1585513826 -7200
# Node ID 189f174792757e33c8d92681e16178e9d0ce2f3e
# Parent  f0499449e149fa117d8adc6434a444ab2edd2b9e
tuned;

diff -r f0499449e149 -r 189f17479275 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Mar 29 22:23:33 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sun Mar 29 22:30:26 2020 +0200
@@ -292,8 +292,8 @@
             }
 
           process.result(
-            progress_stdout = (line: String) =>
-              line match {
+            progress_stdout =
+              {
                 case Loading_Theory_Marker(theory) =>
                   progress.theory(Progress.Theory(theory, session = name))
                 case Protocol.Export.Marker((args, path)) =>