diff options
| author | Hugo Herbelin | 2020-07-24 22:35:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-07-24 22:37:33 +0200 |
| commit | 56ab65848cb894bfe656022b17d1e1687811708a (patch) | |
| tree | d2140426953383e8af4269c6680f21be9ccecc30 /dev/include_printers | |
| parent | e9061bb414dfebad5bdf2efe634030563f8a2381 (diff) | |
Fixes #12752 (applying symbol escaping in index produced by coqdoc).
This is to avoid collision with the syntax of the host output language.
Diffstat (limited to 'dev/include_printers')
0 files changed, 0 insertions, 0 deletions