diff --git a/docs/build.tex b/docs/build.tex
index 9dfce59372..82e7b0b8df 100644
--- a/docs/build.tex
+++ b/docs/build.tex
@@ -547,7 +547,7 @@ The script \texttt{./scripts/env} is used to manage these environments, it uses
 
 The command 
 \begin{Verbatim}
-  \texttt{./scripts/env help}
+  ./scripts/env help
 \end{Verbatim}
 produces a short help text with a list of commands.