From 1fb883aaf4dc0b1111befd7a44395de76547c330 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 4 Dec 2013 15:50:12 +0100
Subject: Documentation of the Derive plugin.

I put it in a new chapter of the Addendum of the manual. Which is meant to be dedicated to plugins with short documentation.---
 doc/refman/Reference-Manual.tex | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc')

diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 7b6c8ba3be..152bdb3eee 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -122,6 +122,7 @@ Options A and B of the licence are {\em not} elected.}
 \include{Polynom.v}%  = Ring
 \include{Nsatz.v}%
 \include{Setoid.v}% Tactique pour les setoides
+\include{Misc.v}
 %BEGIN LATEX
 \RefManCutCommand{ENDADDENDUM=\thepage}
 %END LATEX
-- 
cgit v1.2.3