# HG changeset patch
# User wenzelm
# Date 1678530978 -3600
# Node ID 8c64e51d9dde8737c62190ee03ca5f4521327a3f
# Parent  b0a4f8c294460d3adf618445dd2fa2edd6e1d2ff
unused (see 268bf61631ec);

diff -r b0a4f8c29446 -r 8c64e51d9dde src/Pure/System/options.scala
--- 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(