diff options
| -rw-r--r-- | docs/build.tex | 2 |
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. |