diff options
| author | Erik Martin-Dorel | 2019-12-05 01:14:47 +0100 |
|---|---|---|
| committer | GitHub | 2019-12-05 01:14:47 +0100 |
| commit | b893f682a9bbd0f42dfd4501dc0451ab1e4ec713 (patch) | |
| tree | 43042beef7eb7e95bb04c8184f1470f6f7ee3754 /doc | |
| parent | 15ccaec24ce935de366cae08b906c130379758ce (diff) | |
| parent | a920a00ba9dd1a5e5f21cd03c6c565ebb600ffab (diff) | |
Merge pull request #445 from vzaliva/patch-1
Uncommented coq-find-comment-start, coq-find-comment-end as quick fix for #444
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions