diff options
| author | Guillaume Melquiond | 2016-06-03 08:28:57 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-06-03 08:28:57 +0200 |
| commit | c75805f735d6a7f9972fe9ae8214eebc97c20852 (patch) | |
| tree | 43b790f539cfd275502823709aa0de0f7b49e061 /dev | |
| parent | 99881431d7f3050b5062300c28a514ccd04f878b (diff) | |
Make "coqdoc -g --parse-comments" behave properly (bug #4773).
As a side effect, there should be a small speedup when ignoring comments.
This commit also fixes two bugs related to handling "$$" and "#" in
comments.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions