changeset 77614 | b619d80f61fa |
parent 77515 | 6aae7486e94a |
child 77652 | 5f706f7c624b |
--- a/src/Pure/library.scala Sat Mar 11 13:37:58 2023 +0100 +++ b/src/Pure/library.scala Sat Mar 11 14:18:56 2023 +0100 @@ -292,6 +292,9 @@ def if_proper[A](x: Iterable[A], body: => String): String = if (x == null || x.isEmpty) "" else body + def if_proper(b: Boolean, body: => String): String = + if (!b) "" else body + /* reflection */