| changeset 66923 | 914935f8a462 |
| parent 65831 | 3b197547c1d4 |
| child 68953 | 89a12af9c330 |
--- a/src/Pure/System/numa.scala Thu Oct 26 23:31:03 2017 +0200 +++ b/src/Pure/System/numa.scala Fri Oct 27 11:46:03 2017 +0200 @@ -26,7 +26,7 @@ } if (numa_nodes_linux.is_file) { - Library.space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_)) + space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_)) } else Nil }