From 661940fd55a925a6f17f6025f5d15fc9f5647cf9 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 10 Oct 2016 10:59:22 +0200
Subject: Put all plugins behind an "API".

---
 dev/tools/Makefile.devel | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/tools')

diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel
index 8dcc70cf7f..ffdb1bdca9 100644
--- a/dev/tools/Makefile.devel
+++ b/dev/tools/Makefile.devel
@@ -5,7 +5,7 @@
 TOPDIR=.
 BASEDIR=
 
-SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel
+SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel API
 
 default:	usage noargument
 
-- 
cgit v1.2.3