diff options
| author | Pierre-Marie Pédrot | 2020-04-09 12:58:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-09 12:58:14 +0200 |
| commit | d233c495821f5090b9dd37eec5ed07930f66b561 (patch) | |
| tree | 0ef9f8d7c198df86ff48c9dc22458a2119169f3d /doc/plugin_tutorial/tuto1 | |
| parent | 3778576937512bf9deed90de7b5aad75ef5cde13 (diff) | |
| parent | f06d96687e26d3e491de0a234e889e901b32e1ca (diff) | |
Merge PR #12050: Fix a typo in CoqMakefile.in
Reviewed-by: ppedrot
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions