summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-03-03 10:22:27 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-03-03 10:22:27 +0000
commit891377ce1962cdb31357d6580d6546ec22df2b4f (patch)
tree4ff7c38749cc7a4c1af411c5aa3eb7225c4ae6a1 /Makefile
parent018edf2d81bf94197892cf1df221f7eeac1f96f6 (diff)
Switching to the new C parser/elaborator/simplifier
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile10
1 files changed, 1 insertions, 9 deletions
diff --git a/Makefile b/Makefile
index 95eca7d..856d777 100644
--- a/Makefile
+++ b/Makefile
@@ -25,10 +25,7 @@ OCAMLBUILD=ocamlbuild
OCB_OPTIONS=\
-no-hygiene \
-no-links \
- -I extraction $(INCLUDES) \
- -cflags -I,`pwd`/cil/obj/$(ARCHOS) \
- -lflags -I,`pwd`/cil/obj/$(ARCHOS) \
- -libs unix,str,cil
+ -I extraction $(INCLUDES)
VPATH=$(DIRS)
GPATH=$(DIRS)
@@ -89,9 +86,6 @@ extraction:
$(COQEXEC) extraction/extraction.v
cd extraction && ./fixextract
-cil:
- $(MAKE) -j1 -C cil
-
ccomp: driver/Configuration.ml
$(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \
&& rm -f ccomp && ln -s _build/driver/Driver.native ccomp
@@ -111,7 +105,6 @@ runtime:
all:
$(MAKE) proof
- $(MAKE) cil
$(MAKE) extraction
$(MAKE) ccomp
$(MAKE) runtime
@@ -178,7 +171,6 @@ clean:
distclean:
$(MAKE) clean
- rm -rf cil
rm -f Makefile.config
include .depend