diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-06-16 16:29:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-06-16 16:30:04 +0200 |
| commit | b831c43f592dff6cf307add90354c10f30bf5b58 (patch) | |
| tree | d9dd88c54b6744c138d99274039d2f57d8e0c299 /printing | |
| parent | 902032b9293afacd6c3e16e5e161dd678664bd58 (diff) | |
Fix by Enrico on CoqIDE not locating errors anymore since 550da87456a.
Diffstat (limited to 'printing')
0 files changed, 0 insertions, 0 deletions