From ad702b290fcee29305b8a83b7530e24d655b2d7d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 30 Mar 2018 17:34:50 +0200 Subject: [Sphinx] Move chapter 30 to new infrastructure --- Makefile.doc | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'Makefile.doc') diff --git a/Makefile.doc b/Makefile.doc index 0b45b9cec..fc791ce1c 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -60,8 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ - Universes.v.tex \ - Misc.v.tex) + Universes.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ -- cgit v1.2.3