From 3dbe5120fca007b2a54fda8675384975011792b3 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 13 Dec 2019 09:23:55 +0100
Subject: [PATCH] [Server] Make all server requests appear in the doc index.
---
src/plugins/server/request.ml | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/plugins/server/request.ml b/src/plugins/server/request.ml
index 0ec63893fba..75b095985ab 100644
--- a/src/plugins/server/request.ml
+++ b/src/plugins/server/request.ml
@@ -307,7 +307,9 @@ let register_sig (type a b) (s : (a,b) signature) (process : rq -> a -> b) =
doc_input s.input @
doc_output s.output
in
- let _ = Doc.publish ~page:s.page ~name:s.name ~title description [] in
+ let _ =
+ Doc.publish ~page:s.page ~name:s.name ~title ~index:[s.name] description []
+ in
Main.register s.kind s.name processor ;
s.defined <- true
--
GitLab