diff options
| author | Guillaume Melquiond | 2015-01-06 16:03:44 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-01-06 16:03:44 +0100 |
| commit | 91c9e77b8d75a3c04b64337805d2ce335b27c875 (patch) | |
| tree | d98973ff87335bd11994df8ed365b4ddf08f4b2a /plugins/syntax | |
| parent | fb6bee00a1b52aecbdccc76bf3aa6edf6ed3df08 (diff) | |
Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug #3802.)
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions