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))