diff options
| author | Clément Pit-Claudel | 2020-06-07 12:14:15 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-06-07 12:14:15 -0400 |
| commit | aad87d7e7d7b68b13e33f58b8d5b5a6f824d3f38 (patch) | |
| tree | ef5a10d5dbc9d450f2ad5a412dc956060adfd8ea /doc/plugin_tutorial/README.md | |
| parent | d0e4e7e106b7b27340f37c62d4da99ea2cc8e95f (diff) | |
| parent | c964091f01af77bb9aff14cb25bc4d8466c5239d (diff) | |
Merge PR #12473: Match only a single line as the coqtop prompt in coqtop:: directive
Diffstat (limited to 'doc/plugin_tutorial/README.md')
0 files changed, 0 insertions, 0 deletions