src/Pure/System/options.scala
changeset 77614 b619d80f61fa
parent 77613 44f7b76d1106
child 77616 29effd67d8a8
--- a/src/Pure/System/options.scala	Sat Mar 11 13:37:58 2023 +0100
+++ b/src/Pure/System/options.scala	Sat Mar 11 14:18:56 2023 +0100
@@ -250,7 +250,7 @@
   override def toString: String = iterator.mkString("Options(", ",", ")")
 
   private def print_entry(opt: Options.Entry): String =
-    if (opt.public) "public " + opt.print else opt.print
+    if_proper(opt.public, "public ") + opt.print
 
   def print: String = cat_lines(iterator.toList.sortBy(_.name).map(print_entry))