diff -r 11d844d21f5c -r 4f68b165d69e src/Pure/ROOT.scala
--- a/src/Pure/ROOT.scala	Fri Jan 27 13:57:52 2023 +0000
+++ b/src/Pure/ROOT.scala	Fri Jan 27 15:22:26 2023 +0100
@@ -21,3 +21,4 @@
   val proper_string = Library.proper_string _
   def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
 }
+