--- a/src/Pure/System/options.scala Sat Mar 11 11:31:58 2023 +0100
+++ b/src/Pure/System/options.scala Sat Mar 11 11:36:18 2023 +0100
@@ -427,16 +427,6 @@
}
- /* changed options */
-
- def changed(defaults: Options = Options.init(prefs = "")): List[String] =
- (for {
- (name, opt2) <- options.iterator
- opt1 = defaults.get(name)
- if opt1.isEmpty || opt1.get.value != opt2.value
- } yield (name, opt2.value)).toList.sortBy(_._1).map({ case (x, y) => Properties.Eq(x, y) })
-
-
/* save preferences */
def make_prefs(