From ca82e1ff51108a3dac37f52a96f3af4b4e8d1a18 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 7 Mar 2017 11:18:29 +0100
Subject: Farewell decl_mode

This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.
---
 Makefile.common | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index df705034e..c64ae527f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -61,7 +61,7 @@ PLUGINDIRS:=\
   omega		romega 		micromega 	quote \
   setoid_ring 	extraction 	fourier \
   cc 		funind 		firstorder 	derive \
-  rtauto 	nsatz           syntax          decl_mode	btauto \
+  rtauto 	nsatz           syntax          btauto \
   ssrmatching	ltac
 
 SRCDIRS:=\
-- 
cgit v1.2.3