Admin/jenkins/build/ci_build_benchmark.scala

--- a/Admin/jenkins/build/ci_build_benchmark.scala	Fri Sep 16 15:21:21 2016 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala	Fri Sep 16 15:54:50 2016 +0200
@@ -12,6 +12,6 @@
   def post_hook(results: Build.Results) = {}
 
   def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
-    tree.selection()
+    tree.selection(session_groups = List("timing"))
 
 }