aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-ide.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/RefMan-ide.tex')
-rw-r--r--doc/refman/RefMan-ide.tex1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index c6fbd1c538..75f3d18ded 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -1,5 +1,6 @@
\chapter[\Coq{} Integrated Development Environment]{\Coq{} Integrated Development Environment\label{Addoc-coqide}
\ttindex{coqide}}
+%HEVEA\cutname{coqide.html}
The \Coq{} Integrated Development Environment is a graphical tool, to
be used as a user-friendly replacement to \texttt{coqtop}. Its main