src/Pure/Thy/sessions.scala
changeset 71602 d5502ee7c141
parent 71601 97ccf48c2f0c
child 71642 77327455b00d
--- a/src/Pure/Thy/sessions.scala	Fri Mar 27 22:01:27 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 27 22:06:35 2020 +0100
@@ -271,7 +271,7 @@
                   if !ok(path.canonical_file)
                   path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
                 } yield (path1, name)).toList
-              val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).toSet.toList.sorted
+              val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted
 
               val errs1 =
                 for { (path1, name) <- bad }