diff options
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index ebb6290f92..539ef0f410 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -134,9 +134,11 @@ val is_message : Xml_datatype.xml -> bool * since the two phases are performed sequentially) *) val feedback : - ?state_id:Feedback.state_id -> Feedback.feedback_content -> unit + ?state_id:Feedback.state_id -> + ?route:Feedback.route_id -> Feedback.feedback_content -> unit -val set_id_for_feedback : Feedback.edit_or_state_id -> unit +val set_id_for_feedback : + ?route:Feedback.route_id -> Feedback.edit_or_state_id -> unit val set_feeder : (Feedback.feedback -> unit) -> unit (** {6 Utilities} *) |