# HG changeset patch
# User wenzelm
# Date 1553684888 -3600
# Node ID 2d5c313e858258602ef29f7e93e114d88d696d16
# Parent  3fd083253a1cc5bcb560a1d79fc717dcc8b6da9e
more operations;

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)