summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-09-08 16:50:23 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-09-08 16:50:23 +0000
commitc9acadca7c8d5d29dd57b9acba99369067f93ae1 (patch)
tree9041580ba55ec85af830d61c0b566b0432df0319 /Makefile
parent28c04de64220be15c589c4dbe1662b212b6d25b1 (diff)
Updates for IA32-Cygwin.
cparser/Elab.ml: tolerate changes in qualifiers in ?: cfrontend/C2C.ml: revise info attached to atoms; treat inline functions as static. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1506 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile14
1 files changed, 11 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index 4237f2a..752a8e6 100644
--- a/Makefile
+++ b/Makefile
@@ -82,6 +82,14 @@ DRIVER=Compiler.v Complements.v
FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER)
+# Symbolic links vs. copy
+
+ifneq (,$(findstring CYGWIN,$(shell uname -s)))
+SLN=cp
+else
+SLN=ln -s
+endif
+
proof: $(FILES:.v=.vo)
extraction:
@@ -91,15 +99,15 @@ extraction:
ccomp: driver/Configuration.ml
$(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \
- && rm -f ccomp && ln -s _build/driver/Driver.native ccomp
+ && rm -f ccomp && $(SLN) _build/driver/Driver.native ccomp
ccomp.prof: driver/Configuration.ml
$(OCAMLBUILD) $(OCB_OPTIONS) Driver.p.native \
- && rm -f ccomp.prof && ln -s _build/driver/Driver.p.native ccomp.prof
+ && rm -f ccomp.prof && $(SLN) _build/driver/Driver.p.native ccomp.prof
ccomp.byte: driver/Configuration.ml
$(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \
- && rm -f ccomp.byte && ln -s _build/driver/Driver.d.byte ccomp.byte
+ && rm -f ccomp.byte && $(SLN) _build/driver/Driver.d.byte ccomp.byte
runtime:
$(MAKE) -C runtime