changeset 76856 | 90c552d28d36 |
parent 76855 | 5efc770dd727 |
child 76859 | 6e1bf28d5a80 |
--- a/src/Pure/Thy/sessions.scala Sun Jan 01 21:44:08 2023 +0100 +++ b/src/Pure/Thy/sessions.scala Sun Jan 01 22:01:45 2023 +0100 @@ -249,7 +249,7 @@ var cache_sources = Map.empty[JFile, SHA1.Digest] def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = { for { - path <- paths + path <- Library.distinct(paths) file = path.file if cache_sources.isDefinedAt(file) || file.isFile }