From ef6459b00999a29183edc09de9035795ff7912e9 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Tue, 23 Jun 2015 15:39:47 +0200
Subject: Add target to install dev files.

---
 Makefile.common | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index 07df8bb15..5a81dcfbb 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -253,6 +253,10 @@ CSDPCERTCMO:=$(addprefix plugins/micromega/, \
   mutils.cmo 	micromega.cmo \
   sos_types.cmo sos_lib.cmo sos.cmo 	csdpcert.cmo )
 
+DEVPRINTERS:=dev/vm_printers.ml dev/top_printers.ml
+
+DEVFILES:=dev/base_include dev/include
+
 DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
 
 COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo
-- 
cgit v1.2.3