From 633e40b6f925556e94347c348a2804cdc1068d88 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 8 Mar 2017 14:26:00 +0100
Subject: [camlpX] Enrico's changes to camlp4 removal.

This removes some remaining support for camlp4 in the infrastructure
and documents the change.
---
 Makefile.dev | 21 ---------------------
 1 file changed, 21 deletions(-)

(limited to 'Makefile.dev')

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
-- 
cgit v1.2.3