# HG changeset patch
# User wenzelm
# Date 1494232033 -7200
# Node ID 222ed89010084e5b2cb159f8fc13f4fddaf346bf
# Parent  2edb89630a80c96aef7d80cb9c1f884dceb90abd
suppress "Pure" with its special threads=1 (Jenkins log does not provide threads in ISABELLE_BUILD_OPTIONS);

diff -r 2edb89630a80 -r 222ed8901008 src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Mon May 08 10:23:12 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala	Mon May 08 10:27:13 2017 +0200
@@ -56,6 +56,7 @@
     build_log_jobs.map(job_name =>
       Build_Status.Profile("Jenkins " + job_name,
         Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
+        Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " +
         Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))