src/Pure/config.ML
changeset 39811 0659e84bdc5f
parent 39163 4d701c0388c3
child 40291 012ed4426fda