diff options
Diffstat (limited to 'ide/wg_MessageView.ml')
| -rw-r--r-- | ide/wg_MessageView.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 2b03396314..0fc4e47685 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -9,7 +9,6 @@ class type message_view = object inherit GObj.widget - method add_selection_clipboard : GData.clipboard -> unit method clear : unit -> unit method push : Interface.message_level -> string -> unit end @@ -19,6 +18,8 @@ let message_view () : message_view = let view = GText.view ~buffer ~editable:false ~cursor_visible:false ~wrap_mode:`WORD () in + let default_clipboard = GData.clipboard Gdk.Atom.primary in + let _ = buffer#add_selection_clipboard default_clipboard in let () = view#set_left_margin 2 in object inherit GObj.widget view#as_widget @@ -34,7 +35,4 @@ let message_view () : message_view = buffer#insert ~tags msg; buffer#insert ~tags "\n" - method add_selection_clipboard cb = - buffer#add_selection_clipboard cb - end |