diff options
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 2508779e8..015151bc9 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -116,7 +116,7 @@ type message_level = Feedback.message_level = type message = Feedback.message = { message_level : message_level; - message_content : string; + message_content : Xml_datatype.xml; } type logger = message_level -> std_ppcmds -> unit @@ -154,7 +154,7 @@ val std_logger : logger val set_logger : logger -> unit -val log_via_feedback : unit -> unit +val log_via_feedback : (std_ppcmds -> Xml_datatype.xml) -> unit val of_message : message -> Xml_datatype.xml val to_message : Xml_datatype.xml -> message |