--- a/src/Pure/ROOT.scala	Fri Sep 16 16:02:28 2022 +0200
+++ b/src/Pure/ROOT.scala	Fri Sep 16 16:34:45 2022 +0200
@@ -21,3 +21,4 @@
   val proper_string = Library.proper_string _
   def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
 }
+
changeset 76176	d6bd84eb94a3
parent 75393	87ebf5a50283
child 76537	cdbe20024038