diff --git a/.gitignore b/.gitignore
index 6e056235f64c7cd8cd500327d9f0d8ef537e3866..0a653f944d8129668dfeb79de354d6da3f54c9dc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -99,8 +99,8 @@ autom4te.cache
 /doc/code/print_api/dynamic_plugins.mli
 /doc/code/print_api/_build/
 
+/doc/code/builtin
 /doc/code/studia
-
 /doc/code/qed
 /doc/code/wp
 
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 1d56b3e036f9edef42dc574a8e9dda15e66e45e9..4dc4801d439153529e28113c7575eaabeb71230b 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -1375,6 +1375,21 @@ val cancel : unit -> unit
    of the computation, and any exception is re-raised.
    The callback [~on_mute d] is triggered when the deamon has not been yielded
    for a period [d] longer than [~debounce] or 100ms by default.
+
+
+   Illustrative example, where [...] is the debounced time:
+   {[
+       job data :    |<-------------------------------------------------->|<daemon removed>
+       yields   :       x   x  x x    x             x   x    x   xxx xxx
+       trigger  :       |..........   |..........   |..........  |........|..
+       delayed  :                                   !
+       notes    :      (1)           (2)           (3)                   (4)
+   ]}
+
+   1. First yield, normal trigger
+   2. Debounced yields leads to this second trigger
+   3. Delayed warning invoked since there was no yield for more than debounced period
+   4. Final trigger, a bit before the debounced time
 *)
 val with_progress : ?debounced:int -> ?delayed:(int -> unit) ->
   (unit -> unit) -> ('a -> 'b) -> 'a -> 'b