timeout counts as regular error, with rc = 1 (cf. special Exn.Interrupt vs. regular TimeLimit.TimeOut in Isabelle/ML);
authorwenzelm
Fri, 17 May 2013 21:15:33 +0200
changeset 52063 fd533ac64390
parent 52062 4f91262e7f33
child 52064 4b4ff1d3b723
timeout counts as regular error, with rc = 1 (cf. special Exn.Interrupt vs. regular TimeLimit.TimeOut in Isabelle/ML);
src/Pure/System/isabelle_system.scala
src/Pure/Tools/build.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,
--- 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
     }
   }