aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/RefMan-ide.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/RefMan-ide.tex')
-rw-r--r--doc/RefMan-ide.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan-ide.tex b/doc/RefMan-ide.tex
index c38388c54..aa80bcb5a 100644
--- a/doc/RefMan-ide.tex
+++ b/doc/RefMan-ide.tex
@@ -1,5 +1,5 @@
\chapter{\Coq{} Integrated Development Environment}
-%\label{Addoc-coqide}
+\label{Addoc-coqide}
\ttindex{coqide}
The \Coq{} Integrated Development Environment is a graphical tool, to