diff options
| author | Hugo Herbelin | 2015-06-16 16:29:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-06-16 16:30:04 +0200 |
| commit | b831c43f592dff6cf307add90354c10f30bf5b58 (patch) | |
| tree | d9dd88c54b6744c138d99274039d2f57d8e0c299 | |
| parent | 902032b9293afacd6c3e16e5e161dd678664bd58 (diff) | |
Fix by Enrico on CoqIDE not locating errors anymore since 550da87456a.
| -rw-r--r-- | ide/coqOps.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index af728471f7..2387d65c30 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -655,8 +655,6 @@ object(self) buffer#remove_tag Tags.Script.unjustified ~start ~stop; buffer#remove_tag Tags.Script.tooltip ~start ~stop; buffer#remove_tag Tags.Script.to_process ~start ~stop; - buffer#remove_tag Tags.Script.error ~start ~stop; - buffer#remove_tag Tags.Script.error_bg ~start ~stop; buffer#move_mark ~where:start (`NAME "start_of_input") end; List.iter (fun { start } -> buffer#delete_mark start) seg; |
