diff options
| author | Enrico Tassi | 2014-09-08 13:15:58 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-09-09 13:11:38 +0200 |
| commit | de5ed8e17df8433d4f0ffe6a6440505b5a530638 (patch) | |
| tree | 8660ea9edb389bd60a1beb98f7b11192c55c33a3 | |
| parent | 4d601a87b775529b7d516fa213c688b6ecf5246d (diff) | |
IDE: disable editable text area underline when -debug
This way a user *can* use coqide with -debug
| -rw-r--r-- | ide/session.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/session.ml b/ide/session.ml index 254c53cd62..3acd32d7d2 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 |