diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-17 15:24:17 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-17 15:24:17 +0100 |
| commit | 20c70573181f81c99ea4e8797615dac8308a9b18 (patch) | |
| tree | 5961b1f9c653e6ded4a1c180bb7794930a587425 /Makefile | |
| parent | 0c80820c3850fa2b0713f7519c7085e949cc7cb2 (diff) | |
| download | compcert-20c70573181f81c99ea4e8797615dac8308a9b18.tar.gz compcert-20c70573181f81c99ea4e8797615dac8308a9b18.zip | |
Use OCaml's .opt compilers when available.
Cleanups in configure.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 16 |
1 files changed, 9 insertions, 7 deletions
@@ -135,25 +135,27 @@ extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMach .depend.extr: extraction/STAMP tools/modorder $(MAKE) -f Makefile.extr depend -ccomp: .depend.extr compcert.ini +ccomp: .depend.extr compcert.ini FORCE $(MAKE) -f Makefile.extr ccomp -ccomp.byte: .depend.extr compcert.ini +ccomp.byte: .depend.extr compcert.ini FORCE $(MAKE) -f Makefile.extr ccomp.byte -cchecklink: .depend.extr compcert.ini +cchecklink: .depend.extr compcert.ini FORCE $(MAKE) -f Makefile.extr cchecklink -cchecklink.byte: .depend.extr compcert.ini +cchecklink.byte: .depend.extr compcert.ini FORCE $(MAKE) -f Makefile.extr cchecklink.byte -clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo +clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo FORCE $(MAKE) -f Makefile.extr clightgen -clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo +clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo FORCE $(MAKE) -f Makefile.extr clightgen.byte runtime: $(MAKE) -C runtime -.PHONY: proof extraction runtime +FORCE: + +.PHONY: proof extraction runtime FORCE documentation: doc/coq2html $(FILES) mkdir -p doc/html |