src/Pure/config.ML
changeset 69118 12dce58bcd3f
parent 68827 1286ca9dfd26
child 69574 b4ea943ce0b7