SVN-Revision: 13766
@ -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.