src/Pure/Tools/build.scala
changeset 56871 d06ff36b4fa7
parent 56861 5f827142d89a
child 56873 f7c793b7fe7d
--- a/src/Pure/Tools/build.scala	Mon May 05 17:48:55 2014 +0200
+++ b/src/Pure/Tools/build.scala	Mon May 05 20:10:33 2014 +0200
@@ -599,7 +599,8 @@
             info.options.int("process_output_limit") match {
               case 0 => None
               case m => Some(m * 1000000L)
-            })
+            },
+          strict = false)
       }
 
     def terminate: Unit = thread.interrupt