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 }