diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index dfb77e7987..52dc36b575 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -852,6 +852,15 @@ go();; This command executes the vernacular command \textrm{\textsl{command}} and display the time needed to execute it. + +\subsection[\tt Timeout \textrm{\textsl{int}} \textrm{\textsl{command}}.]{\tt Timeout \textrm{\textsl{int}} \textrm{\textsl{command}}.\comindex{Timeout} +\label{time}} + +This command executes the vernacular command \textrm{\textsl{command}}. If +the command has not terminated after the time specified by the integer +(time expressed in seconds), then it is interrupted and an error message +is displayed. + \section{Controlling display} \subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent} |