diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-01 10:42:22 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-01 10:42:22 +0200 |
| commit | 99d46d24e0282c3e4c5fe8765f4e755a1b3b0253 (patch) | |
| tree | 39903d10bc247366f138639f5c692de4c912221f /Makefile.extr | |
| parent | 0484af01a43f5e0228a2748c7ec06e6557bd63e1 (diff) | |
| download | compcert-kvx-99d46d24e0282c3e4c5fe8765f4e755a1b3b0253.tar.gz compcert-kvx-99d46d24e0282c3e4c5fe8765f4e755a1b3b0253.zip | |
ccomp.force target for forcing compilation without Coq processing
Diffstat (limited to 'Makefile.extr')
| -rw-r--r-- | Makefile.extr | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Makefile.extr b/Makefile.extr index 1a894a16..75eb6dca 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -93,6 +93,10 @@ ccomp: $(CCOMP_OBJS) @echo "Linking $@" @$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+ +# DM force compilation without checking dependencies +ccomp.force: + $(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $(CCOMP_OBJS) + ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" @$(OCAMLC) -o $@ $(LIBS_BYTE) $+ |