From c24c58d9e490d5bdadf6a3b343a34f1cd3c18a72 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 17 Feb 2023 15:27:56 +0100
Subject: [PATCH] [server] fix server doc
---
src/plugins/server/server_doc.ml | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml
index 3209946010d..70e09cf5f95 100644
--- a/src/plugins/server/server_doc.ml
+++ b/src/plugins/server/server_doc.ml
@@ -195,12 +195,11 @@ let descr_of_decl names decl =
let declaration page names decl =
match decl.d_kind with
- | D_decoder _ | D_order _ -> ()
+ | D_decoder _ | D_order _ | D_default _ -> ()
| _ ->
let name = decl.d_ident.name in
let fullname = name_of_ident decl.d_ident in
let kind = kind_of_decl decl.d_kind in
- (* let title = Printf.sprintf "`%s` %s" kind fullname in *)
let title = Printf.sprintf "%s (`%s`)" fullname kind in
let index = [ title ] in
let contents = Markdown.par decl.d_descr in
--
GitLab