diff options
| author | Hugo Herbelin | 2020-04-14 22:19:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-14 22:19:39 +0200 |
| commit | e56ac87a12db577ec5f9b6ab521245e9a60f4812 (patch) | |
| tree | 490a0f03adc2f983491bdd20e80a0dec325429bc /doc/plugin_tutorial/tuto1/src | |
| parent | d1bc21a386a814fe86c0ebac58088ce65d015587 (diff) | |
| parent | 41a1d667f4783635e1332b45a6688078711b3907 (diff) | |
Merge PR #12037: coqdoc: Report location of mismatched '[['
Reviewed-by: herbelin
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src')
0 files changed, 0 insertions, 0 deletions