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.---
 Makefile.common | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index d74f143bd1..b13e828c4e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -122,7 +122,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \
   Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
   Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
-  Setoid.v.tex Helm.tex Classes.v.tex )
+  Setoid.v.tex Helm.tex Classes.v.tex Misc.v.tex)
 
 REFMANTEXFILES:=$(addprefix doc/refman/, \
   headers.sty Reference-Manual.tex \
-- 
cgit v1.2.3