aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-01-05 13:51:59 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-01-05 13:51:59 +0000
commitdeebc6faa91e82cb4a374c3c0eca998f4e536921 (patch)
tree80e642366de657c1b4bfcd5ed44c77ac42d3c0b4 /Makefile
parentbd6a21e2e7c87725b9a1992e0179dae1009e7d40 (diff)
downloadcompcert-deebc6faa91e82cb4a374c3c0eca998f4e536921.tar.gz
compcert-deebc6faa91e82cb4a374c3c0eca998f4e536921.zip
Updates
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile11
1 files changed, 9 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 7c92a334..01bb8be3 100644
--- a/Makefile
+++ b/Makefile
@@ -18,6 +18,7 @@ COQDOC=coqdoc
OCAMLBUILD=ocamlbuild
OCB_OPTIONS=\
-no-hygiene \
+ -no-links \
-I extraction $(INCLUDES) \
-cflags -I,`pwd`/cil/obj/$(ARCHOS) \
-lflags -I,`pwd`/cil/obj/$(ARCHOS) \
@@ -83,10 +84,15 @@ extraction:
$(MAKE) -C extraction
cil:
- $(MAKE) -C cil
+ $(MAKE) -j1 -C cil
ccomp:
- $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native && mv Driver.native ccomp
+ $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \
+ && rm -f ccomp && ln -s _build/driver/Driver.native ccomp
+
+ccomp.byte:
+ $(OCAMLBUILD) $(OCB_OPTIONS) Driver.byte \
+ && rm -f ccomp.byte && ln -s _build/driver/Driver.byte ccomp.byte
runtime:
$(MAKE) -C runtime
@@ -138,6 +144,7 @@ install:
clean:
rm -f $(patsubst %, %/*.vo, $(DIRS))
+ rm -f ccomp ccomp.byte
rm -rf _build
rm -rf doc/html doc/*.glob
rm -f doc/removeproofs.ml doc/removeproofs