From ccd68208146e87b9f185f543aadccc1110e72642 Mon Sep 17 00:00:00 2001
From: Sébastien Dailly <sebastien@chimrod.com>
Date: Thu, 25 Feb 2021 08:41:50 +0100
Subject: Update editor

---
 editor/plugins.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'editor/plugins.ml')

diff --git a/editor/plugins.ml b/editor/plugins.ml
index 6173c4f..8dd960a 100755
--- a/editor/plugins.ml
+++ b/editor/plugins.ml
@@ -127,7 +127,6 @@ let default pm schema =
   (* Add the custom keymaps in the list *)
   let _ = setup##unshift keymaps in
   let _ = setup##push (input_rule pm) in
-  let _ = setup##push (Tooltip.tooltip_plugin pm) in
   let _ = setup##push (Tooltip.bold_plugin pm) in
 
 
-- 
cgit v1.2.3