src/Pure/config.ML
changeset 44057 fda143b5c2f5
parent 40291 012ed4426fda
child 47814 53668571d300
equal deleted inserted replaced
44056:be825a69fc67 44057:fda143b5c2f5