author | wenzelm |
Fri, 09 Oct 2015 17:15:53 +0200 | |
changeset 61375 | 0f91067f6f73 |
parent 61374 | b3c665940d62 |
child 61376 | 93224745477f |
--- a/src/Pure/Tools/build.scala Fri Oct 09 16:58:24 2015 +0200 +++ b/src/Pure/Tools/build.scala Fri Oct 09 17:15:53 2015 +0200 @@ -952,7 +952,7 @@ val browser_chapters = (for { (name, result) <- results.iterator - if result.rc == 0 + if result.rc == 0 && !is_pure(name) info = full_tree(name) if info.options.bool("browser_info") } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).