From 9883bde37482632e135895d75fae973ef8b89a08 Mon Sep 17 00:00:00 2001
From: charguer
Date: Wed, 26 Sep 2018 15:30:21 +0200
Subject: cosmetic changes

---
 ide/wg_ScriptView.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide/wg_ScriptView.mli')

diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index ca35b7fb67..df475f0e66 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -26,7 +26,7 @@ object
   method set_show_right_margin : bool -> unit
   method comment : unit -> unit
   method uncomment : unit -> unit
-  method apply_unicode_binding : unit -> unit (* (string -> unit) -> unit *)
+  method apply_unicode_binding : unit -> unit
   method recenter_insert : unit
   method complete_popup : Wg_Completion.complete_popup
 end
-- 
cgit v1.2.3