aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--docs/build.tex2
1 files changed, 1 insertions, 1 deletions
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.