--- a/Admin/jenkins/build/ci_build_benchmark.scala Tue Jul 05 23:39:49 2016 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala Wed Jul 06 13:45:52 2016 +0200
@@ -5,16 +5,13 @@
def threads = 8
def jobs = 2
- def all = false
- def groups = Nil
- def exclude = Nil
def include = Nil
def select = List(Path.explode("$ISABELLE_HOME/src/Benchmarks"))
def pre_hook(args: List[String]) = {}
def post_hook(results: Build.Results) = {}
- override def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
+ def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
tree.selection()
}