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