# HG changeset patch
# User wenzelm
# Date 1493634513 -7200
# Node ID c84db5e0dd6d98084a7f0cc35cea8c1450378871
# Parent  61cd86bb9613f4d72475b961cc6c10fa6749d0cd
detect Jenkins log files as well;

diff -r 61cd86bb9613 -r c84db5e0dd6d src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon May 01 11:33:06 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Mon May 01 12:28:33 2017 +0200
@@ -134,7 +134,8 @@
 
     def is_log(file: JFile,
       prefixes: List[String] =
-        List(Build_History.log_prefix, Identify.log_prefix, Isatest.log_prefix, AFP_Test.log_prefix),
+        List(Build_History.log_prefix, Identify.log_prefix, Isatest.log_prefix,
+          AFP_Test.log_prefix, Jenkins.log_prefix),
       suffixes: List[String] = List(".log", ".log.gz", ".log.xz")): Boolean =
     {
       val name = file.getName
@@ -341,6 +342,7 @@
 
   object Jenkins
   {
+    val log_prefix = "jenkins_"
     val engine = "jenkins"
     val Host = new Regex("""^Building remotely on (\S+) \((\S+)\).*$""")
     val Start = new Regex("""^Started .*$""")