changeset 52063 | fd533ac64390 |
parent 51987 | 7d8e0e3c553b |
child 52067 | 4894df243482 |
--- a/src/Pure/Tools/build.scala Fri May 17 21:06:01 2013 +0200 +++ b/src/Pure/Tools/build.scala Fri May 17 21:15:33 2013 +0200 @@ -558,8 +558,10 @@ args_file.delete timer.map(_.cancel()) - if (res.rc == 130) - res.add_err(if (timeout) "*** Timeout" else "*** Interrupt") + if (res.rc == 130) { + if (timeout) res.add_err("*** Timeout").set_rc(1) + else res.add_err("*** Interrupt") + } else res } }