From f1315c761dad2b71debeb0f3b81274ac5f6db6e7 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 14 Mar 2018 11:23:15 +0100
Subject: [Sphinx] Move chapter 12 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 e63e6731ec..9545a47c9b 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -109,7 +109,6 @@ Options A and B of the licence are {\em not} elected.}
 \include{RefMan-ssr}
 
 \part{User extensions}
-\include{RefMan-syn.v}% The Syntax and the Grammar commands
 %%SUPPRIME \include{RefMan-tus.v}% Writing tactics
 \include{RefMan-sch.v}% The Scheme commands
 
-- 
cgit v1.2.3