From af4c91877bb8a34b8f1d0b2c01ed1940ab33514f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Mar 2018 10:00:00 +0100
Subject: [Sphinx] Move chapter 15 to new infrastructure

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

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

diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 8909c0fefd..d61c70d64e 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -105,12 +105,6 @@ Options A and B of the licence are {\em not} elected.}
 \lstset{moredelim=[is][]{|*}{*|}}
 \lstset{moredelim=*[is][\itshape\rmfamily]{/*}{*/}}
 
-\part{User extensions}
-%%SUPPRIME \include{RefMan-tus.v}% Writing tactics
-
-\part{Practical tools}
-\include{RefMan-uti}% utilities (gallina, do_Makefile, etc)
-
 %BEGIN LATEX
 \RefManCutCommand{BEGINADDENDUM=\thepage}
 %END LATEX
-- 
cgit v1.2.3