From c742837cfb07e1ca5fac296ab5ae86b33ded8b9d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Mon, 10 Oct 2022 11:48:48 +0200 Subject: [PATCH] [server] plugins table-of-contents --- src/plugins/server/server_doc.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml index a1c14afd4fd..cac5ea51a26 100644 --- a/src/plugins/server/server_doc.ml +++ b/src/plugins/server/server_doc.ml @@ -80,6 +80,10 @@ let page chapter ~title ?(descr=[]) ?readme ~filename () = chapter ; title ; descr ; readme ; sections=[] ; } in + begin match chapter with + | `Kernel | `Protocol -> () + | `Plugin p -> plugins := p :: !plugins + end ; pages := Pages.add path page !pages ; page let static () = [] @@ -239,7 +243,7 @@ let table_of_contents () = List.concat (List.map (fun p -> table_of_chapter (`Plugin p)) - (List.sort String.compare !plugins)) + (List.sort_uniq String.compare !plugins)) module Cmap = Map.Make (struct -- GitLab