src/Pure/Thy/sessions.scala
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
       }