src/Pure/config.ML
changeset 69194 6d514e128a85
parent 68827 1286ca9dfd26
child 69574 b4ea943ce0b7