equal
deleted
inserted
replaced
71 } yield entry |
71 } yield entry |
72 |
72 |
73 examples() ::: release_notes() ::: main_contents |
73 examples() ::: release_notes() ::: main_contents |
74 } |
74 } |
75 |
75 |
76 object Doc_Names extends Scala.Fun("doc_names") |
76 object Doc_Names extends Scala.Fun_String("doc_names") |
77 { |
77 { |
78 val here = Scala_Project.here |
78 val here = Scala_Project.here |
79 def apply(arg: String): String = |
79 def apply(arg: String): String = |
80 if (arg.nonEmpty) error("Bad argument: " + quote(arg)) |
80 if (arg.nonEmpty) error("Bad argument: " + quote(arg)) |
81 else cat_lines((for (Doc(name, _, _) <- contents()) yield name).sorted) |
81 else cat_lines((for (Doc(name, _, _) <- contents()) yield name).sorted) |