diff -r 44f7b76d1106 -r b619d80f61fa src/Pure/System/options.scala --- 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))