From a2f26ddde0c5ee088a4a65ab9708085c16a8ba48 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 17 Mar 2011 21:46:52 +0000
Subject: An option "Set Default Timeout n."

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13916 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-oth.tex | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index ab8e1531f8..5a564b6765 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -933,6 +933,21 @@ 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.
 
+\subsection[\tt Set Default Timeout \textrm{\textsl{int}}.]{\tt Set
+  Default Timeout \textrm{\textsl{int}}.\comindex{Set Default Timeout}}
+
+After using this command, all subsequent commands behave as if they
+were passed to a {\tt Timeout} command. Commands already starting by
+a {\tt Timeout} are unaffected.
+
+\subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\comindex{Unset Default Timeout}}
+
+This command turns off the use of a defaut timeout.
+
+\subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\comindex{Test Default Timeout}}
+
+This command displays whether some default timeout has be set or not.
+
 \section{Controlling display}
 
 \subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent}
-- 
cgit v1.2.3