src/Pure/Build/resources.ML
changeset 82038 42fe486d38d5
parent 79502 c7a98469c0e7