--- a/src/Pure/System/options.scala Sat Mar 11 11:36:18 2023 +0100
+++ b/src/Pure/System/options.scala Sat Mar 11 11:43:47 2023 +0100
@@ -427,7 +427,7 @@
}
- /* save preferences */
+ /* preferences */
def make_prefs(
defaults: Options = Options.init(prefs = ""),