src/Pure/Tools/plugin.ML
changeset 58928 23d0ffd48006
parent 58668 1891f17c6124
child 59058 a78612c67ec0