aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/README.md
diff options
context:
space:
mode:
authorHugo Herbelin2020-02-25 13:53:03 +0100
committerHugo Herbelin2020-02-28 05:35:56 +0100
commita4d8c9414e65271fc97347ae04b0b431206d33f8 (patch)
treef9510503c5d2bdde643a4e4121fa793f9a9e6651 /doc/plugin_tutorial/README.md
parent02b40f6cdb7ec56f34c6b773b1d7768b4b135fd9 (diff)
Makefile in test-suite: More separation of concerns as suggested by Enrico.
See "https://github.com/coq/coq/pull/10008#discussion_r382899607".
Diffstat (limited to 'doc/plugin_tutorial/README.md')
0 files changed, 0 insertions, 0 deletions