diff --git a/docs/build.tex b/docs/build.tex index 9dfce593727980827de4ce9f670d904b136c6915..82e7b0b8df319aac4c9f4940df4b3910be2029e1 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.