diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-20 15:39:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-20 15:42:47 +0100 |
| commit | faefff6dc380021b3a910bfa815899ce15f8012b (patch) | |
| tree | 4cb6f06fd6ef2d5404923a19a967146f00bb5b3c /ide/wg_MessageView.mli | |
| parent | b092acdcf929af3b16f8445c8e5bb0ced52c3346 (diff) | |
Fixing bug #4073.
Diffstat (limited to 'ide/wg_MessageView.mli')
| -rw-r--r-- | ide/wg_MessageView.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 4dcd7306b..23c94f404 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -25,6 +25,7 @@ class type message_view = method buffer : GText.buffer (** for more advanced text edition *) method modify_font : Pango.font_description -> unit + method refresh_color : unit -> unit end val message_view : unit -> message_view |