diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml index 3209946010d0f6fc891db00d50de9f616994c08c..70e09cf5f959eae2e2ed635df6b79291576e1924 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