trim more thoroughly, e.g. trailing \0 seen on some system;
authorwenzelm
Fri, 11 Nov 2016 17:23:26 +0100
changeset 64497 f6cefd465f86
parent 64496 50806c43e01b
child 64498 bb29e6849a28
trim more thoroughly, e.g. trailing \0 seen on some system;
src/Pure/System/numa.scala
--- a/src/Pure/System/numa.scala	Fri Nov 11 16:52:26 2016 +0100
+++ b/src/Pure/System/numa.scala	Fri Nov 11 17:23:26 2016 +0100
@@ -26,7 +26,7 @@
       }
 
     if (numa_nodes_linux.is_file) {
-      Library.space_explode(',', Library.trim_line(File.read(numa_nodes_linux))).flatMap(read(_))
+      Library.space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
     }
     else Nil
   }