aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorVincent Laporte2019-06-18 14:33:33 +0000
committerVincent Laporte2019-06-18 14:33:33 +0000
commit072d597958dc46788e186ae629dd73ac0def8426 (patch)
tree80a481a4fd0cdf37a6bd03d3bc4cbb2aab27bfee
parent6c53049049781a71e366edd738747f9b30eb5d94 (diff)
Revert "Fix bug #5710"
This reverts commit 6d0083bb07528d7cd7ad2f8815d06a4e41deb16c.
-rw-r--r--ide/coqOps.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 89f9411f06..8da9900724 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -732,7 +732,6 @@ object(self)
let start = self#get_start_of_input in
let stop = self#get_end_of_input in
Minilib.log(Printf.sprintf "cleanup tags %d %d" start#offset stop#offset);
- buffer#remove_tag Tags.Script.sentence ~start ~stop;
buffer#remove_tag Tags.Script.tooltip ~start ~stop;
buffer#remove_tag Tags.Script.processed ~start ~stop;
buffer#remove_tag Tags.Script.incomplete ~start ~stop;