diff --git a/src/plugins/e-acsl/doc/userman/eacslgcc.tex b/src/plugins/e-acsl/doc/userman/eacslgcc.tex index 63c7fa7c482a5d2a1289a4a183b0185519b0733e..43f8e99a9d6c86f50f0400b74b6a4873d9846237 100644 --- a/src/plugins/e-acsl/doc/userman/eacslgcc.tex +++ b/src/plugins/e-acsl/doc/userman/eacslgcc.tex @@ -155,7 +155,7 @@ option that suppresses any output except errors or warnings issued by \gcc, \framac or \eacslgcc itself. The output of \eacslgcc can also be redirected to a specified file using the -\texttt{-s} option. For example, the following command will redirect all +\texttt{-s} option. For example, the following command redirects all output during instrumentation and compilation of \texttt{foo.c} to the file named \texttt{/tmp/log}.