aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto2/src/dune
diff options
context:
space:
mode:
authorThéo Zimmermann2020-06-04 18:38:02 +0200
committerThéo Zimmermann2020-06-04 19:27:20 +0200
commit08e73f23b7fd26bf84f9b36156f9ac9cab51ac4d (patch)
tree144ec4ffee609101c1ca0bd1884127fa9e4bf2ef /doc/plugin_tutorial/tuto2/src/dune
parentdb768e6828af62e06eb03d36509be6f8fc1efbf3 (diff)
Document known issue of Proof <term> with PG.
See #12444.
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src/dune')
0 files changed, 0 insertions, 0 deletions