From 1556a040a1703a054fd8045a914f5ab83092810f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 17 Jan 2020 09:29:54 +0100
Subject: [PATCH] [server] cleaning option documentation
---
src/plugins/server/server_parameters.ml | 32 +++++++++++++++++--------
1 file changed, 22 insertions(+), 10 deletions(-)
diff --git a/src/plugins/server/server_parameters.ml b/src/plugins/server/server_parameters.ml
index 57dbdd133f9..0b00960d594 100644
--- a/src/plugins/server/server_parameters.ml
+++ b/src/plugins/server/server_parameters.ml
@@ -33,22 +33,40 @@ module P = Plugin.Register
include P
+(* -------------------------------------------------------------------------- *)
+(* --- Server General Options --- *)
+(* -------------------------------------------------------------------------- *)
+
module Idle = P.Int
(struct
let option_name = "-server-idle"
let arg_name = "ms"
- let default = 20
- let help = "Waiting time (in milliseconds) when idle"
+ let default = 50
+ let help = "Server polling (in milliseconds, default 50ms)"
end)
module Yield = P.Int
(struct
let option_name = "-server-yield"
let arg_name = "ms"
- let default = 20
- let help = "Yielding time (in milliseconds) during computations"
+ let default = 50
+ let help = EXEC yield period (in milliseconds, default 50ms)"
end)
+module Log = P.False
+ (struct
+ let option_name = "-server-logs"
+ let help = "Start monitoring logs before server is running (default is false)"
+ end)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Doc Options --- *)
+(* -------------------------------------------------------------------------- *)
+
+let server_doc = add_group "Server Doc Generation"
+let () = Parameter_customize.set_group server_doc
+let () = Parameter_customize.do_not_save ()
+
module Doc = P.String
(struct
let option_name = "-server-doc"
@@ -57,12 +75,6 @@ module Doc = P.String
let help = "Output a markdown documentation of the server in <dir>"
end)
-module Log = P.False
- (struct
- let option_name = "-server-logs"
- let help = "Start (or stop) monitoring logs"
- end)
-
let wpage = register_warn_category "inconsistent-page"
let wkind = register_warn_category "inconsistent-kind"
let wname = register_warn_category "invalid-name"
--
GitLab