# HG changeset patch
# User wenzelm
# Date 1495402906 -7200
# Node ID 744878d72021ef5a9a33dd58486ce2cb03b1ee3d
# Parent  54f621d5fa005ea62841b91dd1f3473e2fb8569b
more general workaround for failed sessions (again, see also 2edb89630a80, ed7b5cd3a7f2);

diff -r 54f621d5fa00 -r 744878d72021 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sun May 21 23:10:39 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Sun May 21 23:41:46 2017 +0200
@@ -166,7 +166,7 @@
             {
               val threads1 =
                 res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
-                  case Threads_Option(Value.Int(i)) if session_name == "Pure" => i
+                  case Threads_Option(Value.Int(i)) => i
                   case _ => 1
                 }
               val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1)