src/Pure/Admin/afp.scala
changeset 69976 98a440cfbb2b
parent 69975 35cc58a54ffc
child 69977 3c166df11085
     1.1 --- a/src/Pure/Admin/afp.scala	Mon Mar 25 14:40:28 2019 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Mar 25 14:47:54 2019 +0100
     1.3 @@ -28,6 +28,11 @@
     1.4    /* entries */
     1.5  
     1.6    sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
     1.7 +  {
     1.8 +    def maintainers: List[String] =
     1.9 +      Library.space_explode(',', Properties.get(metadata, "notify").getOrElse("")).
    1.10 +        map(_.trim).filter(_.nonEmpty)
    1.11 +  }
    1.12  }
    1.13  
    1.14  class AFP private(options: Options, val base_dir: Path)
    1.15 @@ -68,7 +73,8 @@
    1.16          case Section(name) => flush(); section = name
    1.17          case Property(a, b) =>
    1.18            if (section == "") err("Property without a section")
    1.19 -          props = (a -> b.trim) :: props
    1.20 +          val c = b.trim
    1.21 +          if (c.nonEmpty) props = (a -> c) :: props
    1.22          case Extra_Line(line) =>
    1.23            props match {
    1.24              case Nil => err("Extra line without a property")