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) } } }