src/Pure/System/components.scala
changeset 83371 0e2e5adbdea5
parent 82145 5b8639cb0d11
--- a/src/Pure/System/components.scala	Thu Oct 23 18:00:28 2025 +0200
+++ b/src/Pure/System/components.scala	Thu Oct 23 20:09:14 2025 +0200
@@ -225,7 +225,7 @@
             for (case (a, b) <- File.read_props(props_path).asScala.toList)
               yield {
                 if (!default_platforms.defined(a)) error("Bad platform family " + quote(a))
-                val ps = List.from(b.split("\\s+").iterator.filter(_.nonEmpty)).map(Path.explode)
+                val ps = Word.explode(b).map(Path.explode)
                 for (p <- ps if !p.all_basic) error("Bad path outside component " + p)
                 a -> ps
               }