diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex index 099980681bbc7495273ca9b0a0e83435773c346d..abb1fbebdafec860423b577526ff7b0f0bf86d7a 100644 --- a/doc/userman/user-start.tex +++ b/doc/userman/user-start.tex @@ -266,7 +266,7 @@ content of the file to \texttt{\~{}/.bash\_completion} \item You can \texttt{source} the file, e.g. from your \texttt{.bashrc} with the following command: \begin{verbatim} -source $(frama-c -print-share-path)/.autocomplete_frama-c || true +source $(frama-c -print-share-path)/autocomplete_frama-c || true \end{verbatim} \end{itemize}