more operations;

--- a/src/Pure/Admin/afp.scala	Tue Mar 26 22:18:30 2019 +0100
+++ b/src/Pure/Admin/afp.scala	Wed Mar 27 12:08:08 2019 +0100
@@ -34,6 +34,8 @@
     Date(LocalDate.from(t).atStartOfDay(Date.timezone_berlin))
   }
 
+  def trim_mail(s: String): String = s.replaceAll("<[^>]*>", "").trim
+
   sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
   {
     def get(prop: String): Option[String] = Properties.get(metadata, prop)