diff --git a/doc/userman/user-services.tex b/doc/userman/user-services.tex index cc1f485ba93790d1588952824de815faa6ac469f..24aca42be20f94c4c5714a43cd1ca11ecbb66cc6 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 c90a579eeee645e3c8f9a1473db378e5c7d3c3ed..2fb137f37cb2bd8d0cbd8f32739e973cac502831 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 319c04fc20a3670566a429c73c2393888942264f..fd594ab8978b16a1b826b39d655ce54c12cf4752 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.