diff options
| author | Hugo Herbelin | 2021-04-02 20:22:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2021-04-02 20:27:27 +0200 |
| commit | 1fdc02ef7bf0b3d98eb2c69ab5cf8cd84f77b668 (patch) | |
| tree | 129c49b53cbd1c2c053b375dde49749b2ae3ea2b /dev/base_include | |
| parent | 012b8a08f142d39b2211fd52c811f830f88f2075 (diff) | |
Fixes #11690: wrongly toggled coqide printing matching flag; moving raw->nested.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions