aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto0/_CoqProject
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-09-09 06:01:26 +0000
committerGitHub2020-09-09 06:01:26 +0000
commit215d3013312309d47dae01b66b1781b572d30783 (patch)
tree24577158ced51623fda78424ef89c4618cc2c8bb /doc/plugin_tutorial/tuto0/_CoqProject
parent0ab3e7f16064be178e7c48aeef5252cc0d0d3109 (diff)
parentd10c7e19fe760f139f31809975291b955705dc27 (diff)
Merge PR #12905: Lint stdlib with -mangle-names #2
Reviewed-by: anton-trunov Ack-by: jashug Ack-by: olaure01
Diffstat (limited to 'doc/plugin_tutorial/tuto0/_CoqProject')
0 files changed, 0 insertions, 0 deletions