# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1625813314 -7200
# Node ID 76dbf39a708dce8973d824afe044fd2e8baa19d1
# Parent  fe8d0f4da0e658c01ab19ffc3357627eccd103bc
jenkins: add pre/post-hook results for benchmark

diff -r fe8d0f4da0e6 -r 76dbf39a708d Admin/jenkins/build/ci_build_benchmark.scala
--- a/Admin/jenkins/build/ci_build_benchmark.scala	Thu Jul 08 22:58:48 2021 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala	Fri Jul 09 08:48:34 2021 +0200
@@ -9,8 +9,8 @@
   def include = Nil
   def select = List(Path.explode("$ISABELLE_HOME/src/Benchmarks"))
 
-  def pre_hook(args: List[String]) = {}
-  def post_hook(results: Build.Results) = {}
+  def pre_hook(args: List[String]) = Result.ok
+  def post_hook(results: Build.Results) = Result.ok
 
   def selection = Sessions.Selection(session_groups = List("timing"))