aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-14 23:39:52 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-15 14:44:06 +0100
commit0da906f72536020e4ecf9bd3c6765e20c6bfb2bc (patch)
treeec33e77c8d4726cfe42203d00e5103bdf289112a
parent6ccb7cb8f072d08e3f7a401428950bf869fd1742 (diff)
[Sphinx] Move chapter 16 to new infrastructure
-rw-r--r--Makefile.doc2
-rw-r--r--doc/refman/Reference-Manual.tex1
-rw-r--r--doc/sphinx/practical-tools/coqide.rst (renamed from doc/refman/RefMan-ide.tex)0
3 files changed, 1 insertions, 2 deletions
diff --git a/Makefile.doc b/Makefile.doc
index 01f4f34b3..a6d4584d8 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -68,7 +68,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
REFMANTEXFILES:=$(addprefix doc/refman/, \
headers.sty Reference-Manual.tex \
- RefMan-uti.tex RefMan-ide.tex \
+ RefMan-uti.tex \
AsyncProofs.tex RefMan-ssr.tex) \
$(REFMANCOQTEXFILES) \
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 4ddb5e0f2..a6a3670bd 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}
diff --git a/doc/refman/RefMan-ide.tex b/doc/sphinx/practical-tools/coqide.rst
index 2d9853430..2d9853430 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/sphinx/practical-tools/coqide.rst