--- a/src/Pure/ROOT.scala Sat Jan 16 19:25:20 2021 +0100
+++ b/src/Pure/ROOT.scala Sat Jan 16 22:52:43 2021 +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)
}
+