tuned;
authorwenzelm
Sun, 29 Mar 2020 22:30:26 +0200
changeset 71625 189f17479275
parent 71624 f0499449e149
child 71626 4c8edd527940
tuned;
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)) =>