diff options
Diffstat (limited to 'ide/ideutils.mli')
| -rw-r--r-- | ide/ideutils.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 553c4c2bc..e7cfc4390 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -70,3 +70,6 @@ val requote : string -> string val textview_width : #GText.view -> int (** Returns an approximate value of the character width of a textview *) + +val default_logger : Interface.message_level -> string -> unit +(** Default logger. It logs messages that the casual user should not see. *) |