# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1467805552 -7200
# Node ID 28cc90b0e9c28164198ecf4649ae911d83b449b4
# Parent  249fa34faba26e85a39f0fc24fa678d6f45b0cc1
simplify build scripts

diff -r 249fa34faba2 -r 28cc90b0e9c2 Admin/jenkins/build/ci_build_benchmark.scala
--- 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()
 
 }
diff -r 249fa34faba2 -r 28cc90b0e9c2 Admin/jenkins/build/ci_build_makeall.scala
--- 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)
 
 }
diff -r 249fa34faba2 -r 28cc90b0e9c2 src/Pure/Tools/ci_profile.scala
--- 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)
 
 }