aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto2/src/persistent_counter.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-09-29 09:02:05 +0000
committerGitHub2020-09-29 09:02:05 +0000
commitff74bba7c4ef0c6f3e17944b015e05fc23bad1af (patch)
tree4d7ccf4a2eaf50ba4156f5a8040188c649efe893 /doc/plugin_tutorial/tuto2/src/persistent_counter.ml
parent982c28216f3eb49abfd6b97c69b8fc116c813117 (diff)
parentcc4494897f0897f5795c2bd25fc06d4b07c73667 (diff)
Merge PR #13039: Lint stdlib with -mangle-names #3
Reviewed-by: anton-trunov
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src/persistent_counter.ml')
0 files changed, 0 insertions, 0 deletions