aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto2/_CoqProject
diff options
context:
space:
mode:
authorPierre Roux2019-11-10 16:12:04 +0100
committerPierre Roux2019-11-11 17:43:23 +0100
commit09b39c339dd3fe21a0808097b5f7d1ab8cb47031 (patch)
tree40eb1aa01c8ffbc4531c5a4227c07d50b8051bdb /doc/plugin_tutorial/tuto2/_CoqProject
parent69b91851ed5d18f1ca34ef2597f0cf342c10a124 (diff)
Have only one dune rule calling configure
Diffstat (limited to 'doc/plugin_tutorial/tuto2/_CoqProject')
0 files changed, 0 insertions, 0 deletions