# HG changeset patch # User desharna # Date 1625750758 -7200 # Node ID d593d18a7a9250843b4d1988f22c1814795d5359 # Parent 269b2f976100ab566870696aa3f1f442d8015b6c# Parent 39e0c7fac69edfe2db4dc9bc0e80f70895634212 merged diff -r 269b2f976100 -r d593d18a7a92 src/Pure/Admin/ci_profile.scala --- a/src/Pure/Admin/ci_profile.scala Thu Jul 08 15:10:52 2021 +0200 +++ b/src/Pure/Admin/ci_profile.scala Thu Jul 08 15:25:58 2021 +0200 @@ -14,6 +14,13 @@ abstract class CI_Profile extends Isabelle_Tool.Body { + case class Result(rc: Int) + case object Result + { + def ok: Result = Result(0) + def error: Result = Result(1) + } + private def build(options: Options): (Build.Results, Time) = { val progress = new Console_Progress(verbose = true) @@ -100,7 +107,7 @@ print_section("BUILD") println(s"Build started at $start_time") println(s"Isabelle id $isabelle_id") - pre_hook(args) + val pre_result = pre_hook(args) print_section("LOG") val (results, elapsed_time) = build(options) @@ -129,9 +136,9 @@ } } - post_hook(results) + val post_result = post_hook(results) - System.exit(results.rc) + System.exit(List(pre_result.rc, results.rc, post_result.rc).max) } /* profile */ @@ -156,8 +163,8 @@ def include: List[Path] def select: List[Path] - def pre_hook(args: List[String]): Unit - def post_hook(results: Build.Results): Unit + def pre_hook(args: List[String]): Result + def post_hook(results: Build.Results): Result def selection: Sessions.Selection }