From de5ed8e17df8433d4f0ffe6a6440505b5a530638 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 8 Sep 2014 13:15:58 +0200
Subject: IDE: disable editable text area underline when -debug

This way a user *can* use coqide with -debug
---
 ide/session.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide/session.ml')

diff --git a/ide/session.ml b/ide/session.ml
index 254c53cd6..3acd32d7d 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -132,7 +132,7 @@ let set_buffer_handlers
     try ignore(buffer#get_mark (`NAME "stop_of_input"))
     with GText.No_such_mark _ -> assert false in
   let get_insert () = buffer#get_iter_at_mark `INSERT in
-  let debug_edit_zone () = if !Minilib.debug then begin
+  let debug_edit_zone () = if false (*!Minilib.debug*) then begin
     buffer#remove_tag Tags.Script.edit_zone
       ~start:buffer#start_iter ~stop:buffer#end_iter;
     buffer#apply_tag Tags.Script.edit_zone
-- 
cgit v1.2.3