From 0da906f72536020e4ecf9bd3c6765e20c6bfb2bc Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 14 Mar 2018 23:39:52 +0100
Subject: [Sphinx] Move chapter 16 to new infrastructure

---
 doc/refman/Reference-Manual.tex | 1 -
 1 file changed, 1 deletion(-)

(limited to 'doc/refman/Reference-Manual.tex')

diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 4ddb5e0f2a..a6a3670bd0 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -113,7 +113,6 @@ Options A and B of the licence are {\em not} elected.}
 
 \part{Practical tools}
 \include{RefMan-uti}% utilities (gallina, do_Makefile, etc)
-\include{RefMan-ide}% Coq IDE
 
 %BEGIN LATEX
 \RefManCutCommand{BEGINADDENDUM=\thepage}
-- 
cgit v1.2.3