src/Pure/Tools/build.scala
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
     }
   }