src/Pure/General/properties.scala
changeset 71601 97ccf48c2f0c
parent 68018 3747fe57eb67
child 72137 ad277a335aa5
--- a/src/Pure/General/properties.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/properties.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -67,7 +67,7 @@
         XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text))
       xml_cache match {
         case None => ps
-        case Some(cache) => ps.map(cache.props(_))
+        case Some(cache) => ps.map(cache.props)
       }
     }
   }