# HG changeset patch
# User wenzelm
# Date 1678827606 -3600
# Node ID 5cb7fd36223b7e352053d51be973bc6d9c1547a9
# Parent  d15ad84d75f731e354407497175869929866224c
proper sorting of result (amending f458547b4f0f);

diff -r d15ad84d75f7 -r 5cb7fd36223b src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Mar 14 21:01:20 2023 +0100
+++ b/src/Pure/System/options.scala	Tue Mar 14 22:00:06 2023 +0100
@@ -460,7 +460,7 @@
         (name, opt2) <- options.iterator
         opt1 = defaults.get(name)
         if (opt1.isEmpty || opt1.get.value != opt2.value) && filter(opt2)
-      } yield Options.Change(name, opt2.value, opt1.isEmpty))
+      } yield Options.Change(name, opt2.value, opt1.isEmpty)).sortBy(_.name)
   }