diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 2c9097889fe6b3eab1e7409d805cf593136f4890..c2a61d60d94b2842c0e684d69d4ca5c02d042601 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -5,6 +5,7 @@ release. First we list changes of the last release.
 
 \section*{Frama-C+dev}
 \begin{itemize}
+\item \textbf{Normalizing the Source Code:} new usage of \texttt{-machdep}
 \item \textbf{Normalizing the Source Code:} deprecated option \texttt{-c11}
   (enabled by default).
 \end{itemize}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index b748156775df3412b336012ef6b37269a5608bef..b2256fa875b8c8d2cfdd7ed539652bfd0db76be3 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -296,8 +296,11 @@ The list of supported platforms can be obtained by typing:
 \$ frama-c -machdep help
 \end{frama-c-commands}
 
-The process for adding a new platform is described in the Plug-in
-Development Guide~\cite{plugin-dev-guide}.
+Apart from these default platforms, it is possible to give as argument
+to \texttt{-machdep} option the path of a YAML file containing the information
+needed by \FramaC. The Plug-in Development Guide~\cite{plugin-dev-guide} describes
+this format in more detail, as well as the use of the \texttt{make\_machdep.py}
+script to automatically generate it.
 
 \item \optiondef{-}{simplify-cfg} allows \FramaC to remove break, continue and
   switch statements. This option is automatically set by some plug-ins that