# HG changeset patch # User wenzelm # Date 1478881406 -3600 # Node ID f6cefd465f8636f6a03db78dc24dd6f96ff2d5ba # Parent 50806c43e01b6f2628b05e0ace2827538e17e247 trim more thoroughly, e.g. trailing \0 seen on some system; diff -r 50806c43e01b -r f6cefd465f86 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 }