diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-08 14:26:00 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-07 02:56:18 +0200 |
commit | 633e40b6f925556e94347c348a2804cdc1068d88 (patch) | |
tree | b8063831a6a2ca60cf45d903dedf11f83b308fe5 /Makefile.dev | |
parent | 1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 (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.dev | 21 |
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 |