# HG changeset patch # User wenzelm # Date 1614003645 -3600 # Node ID 54065cbf71347bb2a6ad5d35457e2023b155e42d # Parent f0db1e4c89bcfd3c41caa3a4324815dc430997e7 tuned; diff -r f0db1e4c89bc -r 54065cbf7134 src/Pure/Tools/doc.scala --- 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