# HG changeset patch # User wenzelm # Date 1444403753 -7200 # Node ID 0f91067f6f73971f5abe3ae4592409ad21515168 # Parent b3c665940d62632d507f53feba8debb40a8b8515 tuned output; diff -r b3c665940d62 -r 0f91067f6f73 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).