--- a/src/Pure/ROOT.scala	Mon Jun 28 12:29:00 2021 +0200
+++ b/src/Pure/ROOT.scala	Mon Jun 28 13:13:31 2021 +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 73889	5ec68c1a07d8
parent 73710	241cfa881788
child 73910	c678e58cf999