diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli index efe0822a53b112aadc3d0beb52d143f7581bc9fa..565c20806a04f78a636ff9dca8a062f9e6af3b87 100644 --- a/src/kernel_services/plugin_entry_points/db.mli +++ b/src/kernel_services/plugin_entry_points/db.mli @@ -1375,13 +1375,6 @@ val cancel : unit -> unit [job] on [data] while registering [trigger] as temporary (debounced) daemon. The daemon is finally unregistered at the end of the computation. - {b Raises} every exception raised during the execution of [job] on [data]. - - @param debounced the least amount of time, in milliseconds, between two - successive calls to the daemon (default is 0ms). - @param on_delayed the callback invoked as soon as the time since the last - [yield] is greater than [debounced] milliseconds (or 100ms at least). - Illustrative example, where [...] is the debounced time: {[ job data : |<-------------------------------------------------->|<daemon removed> @@ -1391,9 +1384,16 @@ val cancel : unit -> unit notes : (1) (2) (3) ]} - {ol {li First yield, normal trigger.} - {li Debounced yields leads to this second trigger.} - {li Delayed warning invoked since there was no yield for more than debounced period.}} + + First yield, normal trigger. + + Debounced yields leads to this second trigger. + + Delayed warning invoked since there was no yield for more than debounced period. + + Raises every exception raised during the execution of [job] on [data]. + + @param debounced the least amount of time, in milliseconds, between two + successive calls to the daemon (default is 0ms). + @param on_delayed the callback invoked as soon as the time since the last + [yield] is greater than [debounced] milliseconds (or 100ms at least). *) val with_progress : ?debounced:int -> ?on_delayed:(int -> unit) -> diff --git a/src/plugins/server/request.ml b/src/plugins/server/request.ml index ad7f6ec50c6f2a561704bc1a1262dcd84fa444bd..19dc53b676be9a1a01db12b7c54421e0af9a6e9f 100644 --- a/src/plugins/server/request.ml +++ b/src/plugins/server/request.ml @@ -91,7 +91,7 @@ let signal ~page ~name ~descr ?(details=[]) () = let open Markdown in check_name name ; check_page page name ; - let title = Printf.sprintf "`SIGNAL` %s" name in + let title = Printf.sprintf "`SIG` %s" name in let index = [ Printf.sprintf "%s (`SIGNAL`)" name ] in let description = [ Block [Text descr] ; Block details] in let _ =