src/Pure/library.scala
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 */