timeout counts as regular error, with rc = 1 (cf. special Exn.Interrupt vs. regular TimeLimit.TimeOut in Isabelle/ML);
--- 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
}
}