--- 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()
}
--- a/Admin/jenkins/build/ci_build_makeall.scala Tue Jul 05 23:39:49 2016 +0200
+++ b/Admin/jenkins/build/ci_build_makeall.scala Wed Jul 06 13:45:52 2016 +0200
@@ -5,16 +5,13 @@
def threads = 2
def jobs = 3
- def all = true
- def groups = Nil
- def exclude = Nil
def include = Nil
def select = Nil
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(all_sessions = true)
}
--- a/src/Pure/Tools/ci_profile.scala Tue Jul 05 23:39:49 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala Wed Jul 06 13:45:52 2016 +0200
@@ -124,22 +124,12 @@
def threads: Int
def jobs: Int
- def all: Boolean
- def groups: List[String]
- def exclude: List[String]
def include: List[Path]
def select: List[Path]
def pre_hook(args: List[String]): Unit
def post_hook(results: Build.Results): Unit
- def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
- tree.selection(
- requirements = false,
- all_sessions = all,
- exclude_session_groups = exclude,
- exclude_sessions = Nil,
- session_groups = groups,
- sessions = Nil)
+ def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree)
}