diff options
Diffstat (limited to 'manual')
| -rw-r--r-- | manual/command-reference-manual.tex | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index e2d54cb03..a3264b4cd 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -656,6 +656,9 @@ are specified, all parts of design will be removed. -updates try to remove process updates from syncs. + + -runner "<prefix>" + child process wrapping command, e.g., "timeout 30", or valgrind. \end{lstlisting} \section{cd -- a shortcut for 'select -module <name>'} |