src/Pure/General/properties.scala
changeset 81519 cdc43c0fdbfc
parent 80505 e3af424fdd1a
child 83244 b69ffb4051e8
equal deleted inserted replaced
81518:f012cbfd96d0 81519:cdc43c0fdbfc