diff -r 744878d72021 -r 18f5014331a1 src/Pure/Admin/jenkins.scala --- a/src/Pure/Admin/jenkins.scala Sun May 21 23:41:46 2017 +0200 +++ b/src/Pure/Admin/jenkins.scala Sun May 21 23:47:55 2017 +0200 @@ -57,7 +57,8 @@ Build_Status.Profile("jenkins " + job_name, 0, 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))) + Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) + + " AND " + Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name))) /* job info */