src/Pure/config.ML
changeset 49390 a4202c1f4f9d
parent 47814 53668571d300
child 51947 3301612c4893
equal deleted inserted replaced
49389:da621dc65146 49390:a4202c1f4f9d