From 2ad3eaa5e34c8cc1d2e15fbd2f9e8fbae715b2ce Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 16 Mar 2009 13:41:44 +0000
Subject: Makefile: minor improvements

 * no need anymore for special rules for -rectypes: we use it everywhere
 * $(REVISIONCMO) is obsolete
 * avoid triple references to almost all files of kernel/

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11982 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build | 15 ---------------
 1 file changed, 15 deletions(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index ea2fad1284..5d5ff8533a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -768,21 +768,6 @@ toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
 	  $(NATDYNLINKDEF) -impl $< > $@ \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
-# files compiled with -rectypes
-
-define rectypes-rules-template
-$(1:.ml=.cmo): $(1) | $(1).d
-	$(SHOW)'OCAMLC   -rectypes $$<' 
-	$(HIDE)$(OCAMLC) -rectypes $(BYTEFLAGS) -c $$<
-
-$(1:.ml=.cmx): $(1) | $(1).d
-	$(SHOW)'OCAMLOPT -rectypes $$<'
-	$(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $$<
-
-endef
-
-$(foreach f,$(RECTYPESML),$(eval $(call rectypes-rules-template,$(f))))
-
 # pretty printing of the revision number when compiling a checked out
 # source tree
 .PHONY: revision
-- 
cgit v1.2.3