diff options
| author | letouzey | 2012-12-07 15:19:08 +0000 |
|---|---|---|
| committer | letouzey | 2012-12-07 15:19:08 +0000 |
| commit | d039e69266b5f0ccdac05ac7358008f46798efcb (patch) | |
| tree | 643527040747bd9fefdf8f0e37104df0ff18f837 /plugins/xml/xmlcommand.ml | |
| parent | 9555637d4b54e229e604db0bc8777564edd27691 (diff) | |
Coqide: better removal of the error red tag
Instead of trying to limit the retag to the visible zone
(which may be wrong if the user has scrolled), we remove
the red error tag from the whole buffer (this isn't costly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16038 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions