From b6320588bdc54f0239a537339a359baa5e4d07d4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Thu, 2 Jul 2015 14:32:11 +0200
Subject: Revert "Add target to install dev files."

Broke the build.

This reverts commit ef6459b00999a29183edc09de9035795ff7912e9.
---
 Makefile.common | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index 5a81dcfbb..07df8bb15 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -253,10 +253,6 @@ 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