more robust: avoid occasional problems reading this special file (e.g. SSH.Local or "lxcisa0");
authorwenzelm
Wed, 14 Feb 2024 15:29:52 +0100
changeset 79607 118504de9d0d
parent 79606 d1f060886590
child 79608 f1df99019b50
more robust: avoid occasional problems reading this special file (e.g. SSH.Local or "lxcisa0");
src/Pure/Concurrent/multithreading.scala
--- a/src/Pure/Concurrent/multithreading.scala	Wed Feb 14 15:22:21 2024 +0100
+++ b/src/Pure/Concurrent/multithreading.scala	Wed Feb 14 15:29:52 2024 +0100
@@ -26,8 +26,8 @@
       var physical: Option[Int] = None
       var physical_cores = Map.empty[Int, Int]
 
-      val cpuinfo = ssh.read(Path.explode("/proc/cpuinfo"))
-      for (line <- Library.trim_split_lines(cpuinfo)) {
+      val result = ssh.execute("cat /proc/cpuinfo").check
+      for (line <- Library.trim_split_lines(result.out)) {
         line match {
           case Physical(Value.Int(i)) => physical = Some(i)
           case Cores(Value.Int(i))