aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1/_CoqProject
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-01-11 13:59:55 +0100
committerGaëtan Gilbert2019-01-21 13:42:11 +0100
commit9aad49b0655404055c4f0aa96d203a5e6cdcf07e (patch)
tree2540fee74944689b3b935f04edf57d603f45de1e /doc/plugin_tutorial/tuto1/_CoqProject
parentac8c25a9fac51745f0b53162fba48ef5b86d227d (diff)
Move plugin tutorial to team ownership
Diffstat (limited to 'doc/plugin_tutorial/tuto1/_CoqProject')
0 files changed, 0 insertions, 0 deletions