From c7219aeff951fead91fef7f1bb7ffb91617779e4 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 14 Mar 2009 11:29:48 +0000
Subject: RefMan: a label defined twice

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

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 52dc36b575..0f6871f95e 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -854,7 +854,7 @@ 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}}
+\label{timeout}}
 
 This command executes the vernacular command \textrm{\textsl{command}}. If
 the command has not terminated after the time specified by the integer
-- 
cgit v1.2.3