diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml index 2245dbb9e9c0fe5f7890dc65cf32b572fc7d08dd..f11c71db9edc6ebae0cc658d24d0fb4cea727364 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;