# HG changeset patch
# User wenzelm
# Date 1625048120 -7200
# Node ID 743a58b6b2c3345db683cfb24d162582f5c58661
# Parent  0ddb5de0506e075c5bd72372108c1271fd806cab
tuned: prefer Java interfaces;

diff -r 0ddb5de0506e -r 743a58b6b2c3 src/Pure/System/isabelle_env.scala
--- a/src/Pure/System/isabelle_env.scala	Wed Jun 30 11:35:07 2021 +0200
+++ b/src/Pure/System/isabelle_env.scala	Wed Jun 30 12:15:20 2021 +0200
@@ -220,10 +220,9 @@
         if (!res.ok) error(res.out)
 
         for (s <- space_explode('\u0000', Files.readString(settings_file))) {
-          s match {
-            case Properties.Eq(a, b) => settings.put(a, b)
-            case s => if (s.nonEmpty && !s.startsWith("=")) settings.put(s, "")
-          }
+          val i = s.indexOf('=')
+          if (i > 0) settings.put(s.substring(0, i), s.substring(i + 1))
+          else if (i < 0 && s.nonEmpty) settings.put(s, "")
         }
       }
       finally { Files.delete(settings_file) }