aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-09-08 13:07:17 +0000
committerGitHub2020-09-08 13:07:17 +0000
commitbfcd647d26378bb9a654630c5c2379a769cea967 (patch)
tree7b783b726194d1893894ceda3ed21382d841fcb7 /doc/plugin_tutorial
parentebcfaf62423ee8e35167a5f4b275a17bec111180 (diff)
parentbfd9e79245bf6bf6fb8f837fb44d8f4e3f59f0d2 (diff)
Merge PR #12991: [Small typo] Update match.rst
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions