diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-01 12:47:42 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-01 12:47:42 +0000 |
| commit | 2245717b5800da80371952999bc0cff5f75aa490 (patch) | |
| tree | 607052bd5604bdd13e33530bcfa0f6f9e4b25e70 /Makefile | |
| parent | 58fca75f4ab089d21fc4f4a5bdac71d4b79f899f (diff) | |
Continuation of ARM port.
Cleaned up Makefile and SVN properties.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@935 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 23 |
1 files changed, 16 insertions, 7 deletions
@@ -79,17 +79,25 @@ FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) proof: $(FILES:.v=.vo) -exec: - $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native && mv Driver.native ccomp +extraction: + $(MAKE) -C extraction -all: - $(MAKE) proof +cil: $(MAKE) -C cil - $(MAKE) -C extraction - $(MAKE) exec - $(MAKE) -C extraction + +ccomp: + $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native && mv Driver.native ccomp + +runtime: $(MAKE) -C runtime +.PHONY: proof extraction cil ccomp runtime + +extraction: proof +ccomp: cil extraction + +all: proof cil extraction ccomp runtime + documentation: doc/removeproofs @ln -f $(FILES) doc/ @mkdir -p doc/html @@ -143,3 +151,4 @@ distclean: include .depend +FORCE: |