From 310d0f844b837e2f041e3b6b958be5afc75d83ee Mon Sep 17 00:00:00 2001 From: Thibault Martin <thi.martin.pro@pm.me> Date: Wed, 18 Sep 2024 10:10:53 +0200 Subject: [PATCH] [log] Add description for all "*" categories --- src/kernel_services/plugin_entry_points/log.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml index 2245dbb9e9..f11c71db9e 100644 --- a/src/kernel_services/plugin_entry_points/log.ml +++ b/src/kernel_services/plugin_entry_points/log.ml @@ -888,8 +888,11 @@ struct type warn_category = string let categories = ref Category_trie.empty + let categories_help : ((string, string) Hashtbl.t) = Hashtbl.create 5 + let () = Hashtbl.add categories_help "*" "All categories" + let register_category ?(help="No description provided") (s:string) = let l = split_category s in categories := Category_trie.add_structure l !categories; @@ -949,8 +952,11 @@ struct | Some c -> is_debug_key_enabled c let warn_categories = ref Category_trie.empty + let warn_categories_help : ((string, string) Hashtbl.t) = Hashtbl.create 5 + let () = Hashtbl.add warn_categories_help "*" "All warning categories" + let register_warn_category ?(help="No description provided") s = let l = split_category s in warn_categories := Category_trie.add_structure l !warn_categories; -- GitLab