src/Pure/Tools/plugin.ML
changeset 69376 53194e2a969d
parent 69349 7cef9e386ffe
child 69592 a80d8ec6c998