From 89d8ff940b43a5ae36e69d4a955fc2f31f36611b Mon Sep 17 00:00:00 2001 From: Florent Kirchner <florent.kirchner@cea.fr> Date: Thu, 5 Oct 2017 15:24:12 +0200 Subject: [PATCH] [Doc] Fix output of -mdr-h --- src/plugins/markdown-report/mdr_params.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/plugins/markdown-report/mdr_params.ml b/src/plugins/markdown-report/mdr_params.ml index d85dfc394d7..0a576f7ad4c 100644 --- a/src/plugins/markdown-report/mdr_params.ml +++ b/src/plugins/markdown-report/mdr_params.ml @@ -24,7 +24,7 @@ module Gen_draft = False( let option_name = "-mdr-gen-draft" let help = "instead of a full report, generates an empty draft \ - in a format suitable for -mdr-add-remarks" + in a format suitable for -mdr-remarks" end) module Remarks = Empty_string( @@ -32,10 +32,10 @@ struct let option_name = "-mdr-remarks" let arg_name = "f" let help = - "reads <f> to add additional remarks to various sections of the report. \ - must be in a format compatible with the file produced by -mdr-gen-draft. \ + "reads file <f> to add additional remarks to various sections of the report. \ + Must be in a format compatible with the file produced by -mdr-gen-draft. \ Remarks themselves must be written in pandoc's markdown, although this is \ - not enforced by the plug-in." + not enforced by the plug-in" end ) -- GitLab