diff -r 5a476a87a535 -r 914935f8a462 src/Pure/System/numa.scala
--- 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
   }