aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.dev
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-08 14:26:00 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-07 02:56:18 +0200
commit633e40b6f925556e94347c348a2804cdc1068d88 (patch)
treeb8063831a6a2ca60cf45d903dedf11f83b308fe5 /Makefile.dev
parent1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 (diff)
[camlpX] Enrico's changes to camlp4 removal.
This removes some remaining support for camlp4 in the infrastructure and documents the change.
Diffstat (limited to 'Makefile.dev')
-rw-r--r--Makefile.dev21
1 files changed, 0 insertions, 21 deletions
diff --git a/Makefile.dev b/Makefile.dev
index ea6b8b919..5931e46dd 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -20,13 +20,8 @@ DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo
devel: printers
printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp4.dbg
-ifeq ($(CAMLP4),camlp5)
dev/camlp4.dbg:
echo "load_printer gramlib.cma" > $@
-else
-dev/camlp4.dbg:
- echo "load_printer camlp4lib.cma" > $@
-endif
############
# revision
@@ -199,22 +194,6 @@ ltac: $(LTACVO) $(LTACCMO)
.PHONY: omega micromega setoid_ring nsatz extraction
.PHONY: fourier funind cc rtauto btauto ltac
-#################################
-### Misc other development rules
-#################################
-
-# NOTA : otags only accepts camlp4 as preprocessor, so the following rule
-# won't build tags of .ml4 when compiling with camlp5
-
-otags:
- otags $(MLIFILES) $(filter-out configure.ml, $(MLSTATICFILES)) \
- $(if $(filter camlp5,$(CAMLP4)), , \
- -pa op -pa g -pa m -pa rq $(addprefix -pa , $(CAMLP4DEPS)) \
- $(addprefix -impl , $(ML4FILES)))
-
-.PHONY: otags
-
-
# For emacs:
# Local Variables:
# mode: makefile