From 2f30bb4855cc4f3f96aa6904b9b8c48414100bb4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Mon, 12 Mar 2018 22:01:51 +0100
Subject: [Sphinx] Move chapter 2 to new infrastructure

---
 Makefile.doc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.doc')

diff --git a/Makefile.doc b/Makefile.doc
index e6ab89efc..0f99f0530 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -57,7 +57,7 @@ ALLSPHINXOPTS= -d $(SPHINXBUILDDIR)/doctrees $(SPHINXOPTS)
 DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 
 REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
-  RefMan-gal.v.tex RefMan-ext.v.tex \
+  RefMan-gal.v.tex \
   RefMan-mod.v.tex RefMan-tac.v.tex \
   RefMan-cic.v.tex RefMan-lib.v.tex \
   RefMan-tacex.v.tex RefMan-syn.v.tex \
-- 
cgit v1.2.3