# HG changeset patch
# User wenzelm
# Date 1553521674 -3600
# Node ID 98a440cfbb2b47b7e88276ab0cce7e36d1edb76a
# Parent  35cc58a54ffc0176559a21a935a1708da8509e6f
provide maintainers as seen in AFP/admin;
suppress empty properties;

diff -r 35cc58a54ffc -r 98a440cfbb2b src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Mon Mar 25 14:40:28 2019 +0100
+++ b/src/Pure/Admin/afp.scala	Mon Mar 25 14:47:54 2019 +0100
@@ -28,6 +28,11 @@
   /* entries */
 
   sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
+  {
+    def maintainers: List[String] =
+      Library.space_explode(',', Properties.get(metadata, "notify").getOrElse("")).
+        map(_.trim).filter(_.nonEmpty)
+  }
 }
 
 class AFP private(options: Options, val base_dir: Path)
@@ -68,7 +73,8 @@
         case Section(name) => flush(); section = name
         case Property(a, b) =>
           if (section == "") err("Property without a section")
-          props = (a -> b.trim) :: props
+          val c = b.trim
+          if (c.nonEmpty) props = (a -> c) :: props
         case Extra_Line(line) =>
           props match {
             case Nil => err("Extra line without a property")