aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2015-07-02 16:16:46 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-07-02 16:16:46 +0200
commit27de0f2d7e5cd0cc4b221413dfe3c7b739104350 (patch)
treea42625106f71295ebc2011b797603cd1b3b8ec83 /Makefile.common
parenta28d9981e5baf812de14e62de8d904e545e804e5 (diff)
parent44f45f58dc0a169286c9fcfa7d2edbc8bc04673b (diff)
Merge branch 'v8.5' into trunk
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common4
1 files changed, 0 insertions, 4 deletions
diff --git a/Makefile.common b/Makefile.common
index 342ce7727..15ac13ff1 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) lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo