diff options
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)) |