aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--ide/coqOps.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 741a1d6e2a..52f935bf66 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -447,7 +447,6 @@ object(self)
| Processed, Some (id,sentence) ->
log "Processed" id;
remove_flag sentence `PROCESSING;
- remove_flag sentence `ERROR;
self#mark_as_needed sentence
| ProcessingIn _, Some (id,sentence) ->
log "ProcessingIn" id;