# HG changeset patch # User wenzelm # Date 1713262712 -7200 # Node ID d510a1cf9965fa77465c19d3f5f1cffd4261491a # Parent d4d9a7887b2a39543b5b93869c04841d9f43e9aa tuned; diff -r d4d9a7887b2a -r d510a1cf9965 src/Pure/Build/build.scala --- a/src/Pure/Build/build.scala Tue Apr 16 12:08:40 2024 +0200 +++ b/src/Pure/Build/build.scala Tue Apr 16 12:18:32 2024 +0200 @@ -79,10 +79,11 @@ def cache: Term.Cache = store.cache def sessions_ok: List[String] = - (for { - name <- deps.sessions_structure.build_topological_order.iterator - result <- results.get(name) if result.ok - } yield name).toList + List.from( + for { + name <- deps.sessions_structure.build_topological_order.iterator + result <- results.get(name) if result.ok + } yield name) def info(name: String): Sessions.Info = deps.sessions_structure(name) def sessions: Set[String] = results.keySet @@ -231,10 +232,11 @@ if (check_unknown_files) { val source_files = - (for { - (_, base) <- build_deps.session_bases.iterator - (path, _) <- base.session_sources.iterator - } yield path).toList + List.from( + for { + (_, base) <- build_deps.session_bases.iterator + (path, _) <- base.session_sources.iterator + } yield path) Mercurial.check_files(source_files)._2 match { case Nil => case unknown_files =>