From 1532e727b7739fb609113090f5d88301e48ae0a3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 4 Jul 2019 15:45:58 +0200
Subject: [PATCH] [Doc] Documents the new option -explain.
---
doc/userman/user-services.tex | 6 +++---
doc/userman/user-start.tex | 4 ++++
man/frama-c.1.md | 3 +++
3 files changed, 10 insertions(+), 3 deletions(-)
diff --git a/doc/userman/user-services.tex b/doc/userman/user-services.tex
index cc1f485ba93..24aca42be20 100644
--- a/doc/userman/user-services.tex
+++ b/doc/userman/user-services.tex
@@ -89,7 +89,7 @@ loading another project file.
Options \optionuse{-}{help}, \optionuse{-}{verbose},
\optionuse{-}{debug}\xspace(and
their corresponding plugin-specific counterpart)
-as well as \optionuse{-}{quiet}\xspace and
+as well as \optionuse{-}{explain}, \optionuse{-}{quiet}\xspace and
\optionuse{-}{unicode}\xspace are not saved on disk.
\section{Dependencies between Analyses}
@@ -185,5 +185,5 @@ generates (resp. does not generate) a journal upon exiting the session.
Modifications of options \optionuse{-}{help}, \optionuse{-}{verbose},
\optionuse{-}{debug}\xspace (and their corresponding counterpart) as well as
-\optionuse{-}{quiet}\xspace and \optionuse{-}{unicode}\xspace are not written in
-the journal.
+\optionuse{-}{explain}, \optionuse{-}{quiet}\xspace and
+\optionuse{-}{unicode}\xspace are not written in the journal.
diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex
index c90a579eeee..2fb137f37cb 100644
--- a/doc/userman/user-start.tex
+++ b/doc/userman/user-start.tex
@@ -132,6 +132,10 @@ while \optiondef{-}{version} prints the \FramaC version only
The options of the installed plug-ins are displayed by using either the
option \texttt{-<plug-in shortname>-help} or \texttt{-<plug-in shortname>-h}.
+Finally, the option \optiondef{-}{explain} can be used to obtain information
+about some specific options of the kernel or of any installed plug-ins:
+it prints a help message for each other option given in the command line.
+
\subsection{\FramaC Configuration}\label{sec:version}
The complete configuration of \FramaC can be obtained with various options,
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index 319c04fc20a..fd594ab8978 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -55,6 +55,9 @@ option which has the opposite effect.
-kernel-help
: prints the list of options recognized by Frama-C's kernel
+-explain
+: prints a help message for each other option given in the command line
+
-verbose *n*
: sets verbosity level. Defaults to 1.
Setting it to 0 will output less progress messages.
--
GitLab