diff options
| author | Vincent Laporte | 2019-06-18 14:33:33 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-06-18 14:33:33 +0000 |
| commit | 072d597958dc46788e186ae629dd73ac0def8426 (patch) | |
| tree | 80a481a4fd0cdf37a6bd03d3bc4cbb2aab27bfee | |
| parent | 6c53049049781a71e366edd738747f9b30eb5d94 (diff) | |
Revert "Fix bug #5710"
This reverts commit 6d0083bb07528d7cd7ad2f8815d06a4e41deb16c.
| -rw-r--r-- | ide/coqOps.ml | 1 |
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; |
