diff options
| author | Maxime Dénès | 2017-11-03 10:36:11 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-03 10:36:11 +0100 |
| commit | f5108ae3467fb82465778f9c36f609b227f23dc6 (patch) | |
| tree | 10ef692cc8647b09b151a849f93621703185fc52 /dev/base_include | |
| parent | 8964ee7244d702a9a512c683740769e0e5d847d1 (diff) | |
| parent | 6171d9768a03734480233050aa58a6a776726c31 (diff) | |
Merge PR #5999: An attempt to fix issue #5771 (error color hidden by warning color in coqide).
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions