changeset 61375 | 0f91067f6f73 |
parent 61372 | cf40b6b1de54 |
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).