From 072d597958dc46788e186ae629dd73ac0def8426 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 18 Jun 2019 14:33:33 +0000
Subject: Revert "Fix bug #5710"

This reverts commit 6d0083bb07528d7cd7ad2f8815d06a4e41deb16c.
---
 ide/coqOps.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'ide')

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;
-- 
cgit v1.2.3