From b221752b08a3f4a14add245e21ab0e66caa482e2 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 5 Feb 2020 10:04:08 +0100
Subject: [PATCH] [db] Fix some typos.
---
src/kernel_services/plugin_entry_points/db.mli | 8 +++-----
1 file changed, 3 insertions(+), 5 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index b851a5819c3..81a619eb97e 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -1344,7 +1344,6 @@ val progress: (unit -> unit) ref
type daemon
(**
-
[on_progress ?debounced ?on_delayed trigger] registers [trigger] as new
daemon to be executed on each [yield].
@param debounced the least amount of time, in milliseconds, between two
@@ -1399,11 +1398,10 @@ val with_progress :
?debounced:int -> ?on_delayed:(int -> unit) ->
(unit -> unit) -> ('a -> 'b) -> 'a -> 'b
-
(**
- Pauses the currently running process for the specified time, in milli-seconds.
- Registered daemons, if any, will be regularily triggered during this waiting
- time at a reasonnable period with respect to their debouncing constraints.
+ Pauses the currently running process for the specified time, in milliseconds.
+ Registered daemons, if any, will be regularly triggered during this waiting
+ time at a reasonable period with respect to their debouncing constraints.
*)
val sleep : int -> unit
--
GitLab