diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-28 21:31:24 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-28 21:31:24 +0100 |
| commit | 69d6a2c1e08e6169af95bf895d6b0380edb0d081 (patch) | |
| tree | 38ff4dc08878b1f005e4c12c5dfede83e2e04d45 /Makefile | |
| parent | 070adbfa6fbddee552e689bbee4bf76fa4bf770a (diff) | |
| download | compcert-kvx-69d6a2c1e08e6169af95bf895d6b0380edb0d081.tar.gz compcert-kvx-69d6a2c1e08e6169af95bf895d6b0380edb0d081.zip | |
Added configuration to enable clightgen build.
The new configuration option -clightgen activates the build of clightgen.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 16 |
1 files changed, 6 insertions, 10 deletions
@@ -123,10 +123,11 @@ all: ifeq ($(HAS_RUNTIME_LIB),true) $(MAKE) runtime endif -ifeq ($(CCHECKLINK),true) - $(MAKE) cchecklink +ifeq ($(CLIGHTGEN),true) + $(MAKE) clightgen endif + proof: $(FILES:.v=.vo) extraction: extraction/STAMP @@ -144,11 +145,6 @@ ccomp: .depend.extr compcert.ini driver/Version.ml FORCE ccomp.byte: .depend.extr compcert.ini driver/Version.ml FORCE $(MAKE) -f Makefile.extr ccomp.byte -cchecklink: .depend.extr compcert.ini driver/Version.ml FORCE - $(MAKE) -f Makefile.extr cchecklink -cchecklink.byte: .depend.extr compcert.ini driver/Version.ml FORCE - $(MAKE) -f Makefile.extr cchecklink.byte - clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE $(MAKE) -f Makefile.extr clightgen clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE @@ -228,10 +224,10 @@ install: install -m 0755 ./ccomp $(BINDIR) install -d $(SHAREDIR) install -m 0644 ./compcert.ini $(SHAREDIR) -ifeq ($(CCHECKLINK),true) - install -m 0755 ./cchecklink $(BINDIR) -endif $(MAKE) -C runtime install +ifeq ($(CLIGHTGEN),true) + install -m 0755 ./clightgen $(BINDIR) +endif clean: rm -f $(patsubst %, %/*.vo, $(DIRS)) |