tuned output;
authorwenzelm
Fri, 09 Oct 2015 17:15:53 +0200
changeset 61375 0f91067f6f73
parent 61374 b3c665940d62
child 61376 93224745477f
tuned output;
src/Pure/Tools/build.scala
--- 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).