# HG changeset patch
# User wenzelm
# Date 1554891090 -7200
# Node ID d9ea307aac2aae5c764acb9bc18417150e8673fd
# Parent  9b9c1192f9723002ff8036214385e02740c92f3d
tuned;

diff -r 9b9c1192f972 -r d9ea307aac2a src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Tue Apr 09 17:06:15 2019 +0200
+++ b/src/Pure/Admin/afp.scala	Wed Apr 10 12:11:30 2019 +0200
@@ -41,7 +41,7 @@
     def get(prop: String): Option[String] = Properties.get(metadata, prop)
     def get_string(prop: String): String = get(prop).getOrElse("")
     def get_strings(prop: String): List[String] =
-      Library.space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty)
+      space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty)
 
     def title: String = get_string("title")
     def authors: List[String] = get_strings("author")