aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2014-12-17 13:23:51 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2014-12-17 13:23:51 +0100
commita80705575b12c9813d6a7ecf92bb33aedd10b09e (patch)
tree0b260d771fcd5aef702f3389769a6dae65b8e9bf /Makefile
parente86596ae60132b0821cb8b15409074e4cd76243a (diff)
parentc1daedb244d1f7586c12749642b0d78ae910e60a (diff)
downloadcompcert-a80705575b12c9813d6a7ecf92bb33aedd10b09e.tar.gz
compcert-a80705575b12c9813d6a7ecf92bb33aedd10b09e.zip
Merge branch 'master' into dwarf
Conflicts: powerpc/PrintAsm.ml
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile23
1 files changed, 8 insertions, 15 deletions
diff --git a/Makefile b/Makefile
index 60342fa6..56c0cca4 100644
--- a/Makefile
+++ b/Makefile
@@ -31,6 +31,7 @@ COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
COQDOC="$(COQBIN)coqdoc"
COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) -batch -load-vernac-source
COQCHK="$(COQBIN)coqchk" $(COQINCLUDES)
+CP=cp
OCAMLBUILD=ocamlbuild
OCB_OPTIONS=\
@@ -130,14 +131,6 @@ DRIVER=Compopts.v Compiler.v Complements.v
FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \
$(PARSERVALIDATOR) $(PARSER)
-# Symbolic links vs. copy
-
-ifneq (,$(findstring CYGWIN,$(shell uname -s)))
-SLN=cp
-else
-SLN=ln -s
-endif
-
all:
$(MAKE) proof
$(MAKE) extraction
@@ -160,34 +153,34 @@ extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMach
ccomp: extraction/STAMP compcert.ini
$(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \
- && rm -f ccomp && $(SLN) _build/driver/Driver.native ccomp
+ && $(CP) _build/driver/Driver.native ccomp
ccomp.prof: extraction/STAMP compcert.ini
$(OCAMLBUILD) $(OCB_OPTIONS) Driver.p.native \
- && rm -f ccomp.prof && $(SLN) _build/driver/Driver.p.native ccomp.prof
+ && $(CP) _build/driver/Driver.p.native ccomp.prof
ccomp.byte: extraction/STAMP compcert.ini
$(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \
- && rm -f ccomp.byte && $(SLN) _build/driver/Driver.d.byte ccomp.byte
+ && $(CP) _build/driver/Driver.d.byte ccomp.byte
runtime:
$(MAKE) -C runtime
cchecklink: compcert.ini
$(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.native \
- && rm -f cchecklink && $(SLN) _build/checklink/Validator.native cchecklink
+ && $(CP) _build/checklink/Validator.native cchecklink
cchecklink.byte: compcert.ini
$(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.d.byte \
- && rm -f cchecklink.byte && $(SLN) _build/checklink/Validator.d.byte cchecklink.byte
+ && $(CP) _build/checklink/Validator.d.byte cchecklink.byte
clightgen: extraction/STAMP compcert.ini exportclight/Clightdefs.vo
$(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.native \
- && rm -f clightgen && $(SLN) _build/exportclight/Clightgen.native clightgen
+ && $(CP) _build/exportclight/Clightgen.native clightgen
clightgen.byte: extraction/STAMP compcert.ini exportclight/Clightdefs.vo
$(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.d.byte \
- && rm -f clightgen.byte && $(SLN) _build/exportclight/Clightgen.d.byte clightgen.byte
+ && $(CP) _build/exportclight/Clightgen.d.byte clightgen.byte
.PHONY: proof extraction ccomp ccomp.prof ccomp.byte runtime cchecklink cchecklink.byte clightgen clightgen.byte