diff options
| author | Maxime Dénès | 2017-09-07 13:36:32 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-07 13:36:32 +0200 |
| commit | b1fbec7e3945fe2965f4ba9f80c8c31b821dbce1 (patch) | |
| tree | 463fcfdcfdee27e5923e385202ed89a8d4ca4d45 /dev | |
| parent | 0628fc8f0d9afaa9c88c578d1af517c87a28b74c (diff) | |
| parent | 13e33e52869d6c863eaa307f9eb5661b6eeeef93 (diff) | |
Merge PR #997: coqdoc: Support comments in verbatim output
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions