Admin/jenkins/build/ci_build_makeall_seq.scala

--- a/Admin/jenkins/build/ci_build_makeall_seq.scala	Thu Apr 06 21:37:13 2017 +0200
+++ b/Admin/jenkins/build/ci_build_makeall_seq.scala	Fri Apr 07 10:47:25 2017 +0200
@@ -11,7 +11,6 @@
   def pre_hook(args: List[String]) = {}
   def post_hook(results: Build.Results) = {}
 
-  def select_sessions(sessions: Sessions.T) =
-    sessions.selection(all_sessions = true)
+  def selection = Sessions.Selection(all_sessions = true)
 
 }