changeset 73276 | 54065cbf7134 |
parent 72770 | 0c86c29767b2 |
child 73340 | 0ffcad1f6130 |
--- a/src/Pure/Tools/doc.scala Mon Feb 22 14:48:03 2021 +0100 +++ b/src/Pure/Tools/doc.scala Mon Feb 22 15:20:45 2021 +0100 @@ -22,7 +22,7 @@ dir <- dirs() catalog = dir + Path.basic("Contents") if catalog.is_file - line <- split_lines(Library.trim_line(File.read(catalog))) + line <- Library.trim_split_lines(File.read(catalog)) } yield (dir, line) sealed abstract class Entry