# HG changeset patch # User Fabian Huch # Date 1625740768 -7200 # Node ID 39e0c7fac69edfe2db4dc9bc0e80f70895634212 # Parent fa92bc604c596185a4504ab9913104b0182b70b1 jenkins: pre/post-hook results diff -r fa92bc604c59 -r 39e0c7fac69e src/Pure/Admin/ci_profile.scala --- a/src/Pure/Admin/ci_profile.scala Thu Jul 08 08:44:18 2021 +0200 +++ b/src/Pure/Admin/ci_profile.scala Thu Jul 08 12:39:28 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 }