From db293d185f8deb091d4b086f327caa0f376d67d7 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 29 Jan 2015 20:04:22 +0100
Subject: Fix index of reference manual.

---
 doc/refman/RefMan-com.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc/refman/RefMan-com.tex')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index a937332569..49bcdb1db7 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -1,6 +1,7 @@
 \chapter[The \Coq~commands]{The \Coq~commands\label{Addoc-coqc}
 \ttindex{coqtop}
-\ttindex{coqc}}
+\ttindex{coqc}
+\ttindex{coqchk}}
 
 There are three \Coq~commands: 
 \begin{itemize}
-- 
cgit v1.2.3