# HG changeset patch
# User wenzelm
# Date 1368818133 -7200
# Node ID fd533ac64390538eca1d950069a44de21fb792b6
# Parent  4f91262e7f334c0ad5a43df0f56e63495c516e33
timeout counts as regular error, with rc = 1 (cf. special Exn.Interrupt vs. regular TimeLimit.TimeOut in Isabelle/ML);

diff -r 4f91262e7f33 -r fd533ac64390 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri May 17 21:06:01 2013 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri May 17 21:15:33 2013 +0200
@@ -354,6 +354,7 @@
     def out: String = cat_lines(out_lines)
     def err: String = cat_lines(err_lines)
     def add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s))
+    def set_rc(i: Int): Bash_Result = copy(rc = i)
   }
 
   def bash_env(cwd: JFile, env: Map[String, String], script: String,
diff -r 4f91262e7f33 -r fd533ac64390 src/Pure/Tools/build.scala
--- 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
     }
   }