diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-07 11:47:13 -0400 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-07 11:47:13 -0400 |
| commit | 1334a657052a2385c3f3b01cc65c3ccae448fa96 (patch) | |
| tree | 1712481c8883f31567ad09057750a3f24fc26138 /.gitignore | |
| parent | 4dcd50dd2767c60f8f773fb4ca1c3d4bc68819c8 (diff) | |
CoqIDE: remove useless print
There is little point in telling the user the error report is sub optimal.
In this particular case, such error has already been reported (on
the correct location) so reminding it in a non-localized way is not
even that bad.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions