src/Pure/Tools/build.scala
changeset 61375 0f91067f6f73
parent 61372 cf40b6b1de54
child 61376 93224745477f
equal deleted inserted replaced
61374:b3c665940d62 61375:0f91067f6f73
   950 
   950 
   951     if (!no_build) {
   951     if (!no_build) {
   952       val browser_chapters =
   952       val browser_chapters =
   953         (for {
   953         (for {
   954           (name, result) <- results.iterator
   954           (name, result) <- results.iterator
   955           if result.rc == 0
   955           if result.rc == 0 && !is_pure(name)
   956           info = full_tree(name)
   956           info = full_tree(name)
   957           if info.options.bool("browser_info")
   957           if info.options.bool("browser_info")
   958         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   958         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   959             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
   959             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
   960 
   960