diff options
| author | Hugo Herbelin | 2020-04-05 15:14:25 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-05 15:44:18 +0200 |
| commit | f79e15086e9a6f002facd7411971a1f69beac46d (patch) | |
| tree | 0f2022d20eb822694e6cae097d1bb80ab647b435 /tools | |
| parent | ab337ff78d2b5b5bcfc02176357b5f64f3f9ec0c (diff) | |
Quoting _CoqProject in a comment to avoid coqdoc to interpret it as emphasis.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions