diff -r 3fd083253a1c -r 2d5c313e8582 src/Pure/Admin/afp.scala --- 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)