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