src/Pure/config.ML
changeset 56304 40274e4f5ebf
parent 56294 85911b8a6868
child 56438 7f6b2634d853