From 89c3f7e080d66ec8a70ae9dea09ac569158c5313 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 24 Feb 2020 14:53:14 +0100
Subject: [PATCH] [server] generated documentation
---
.../plugin_entry_points/db.mli | 20 +++++++++----------
src/plugins/server/request.ml | 2 +-
2 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index efe0822a53b..565c20806a0 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 ad7f6ec50c6..19dc53b676b 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 _ =
--
GitLab