# HG changeset patch
# User wenzelm
# Date 1678531427 -3600
# Node ID eaa6b47fab2c6953e509ec422205003406f46953
# Parent  8c64e51d9dde8737c62190ee03ca5f4521327a3f
tuned comments;

diff -r 8c64e51d9dde -r eaa6b47fab2c src/Pure/System/options.scala
--- 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 = ""),