From 8c1e56414da2326711efdda18fde7578cc78a373 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 25 May 2020 11:11:06 +0200 Subject: Adding stub RTLpathLivegenaux.ml --- Makefile.extr | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Makefile.extr') diff --git a/Makefile.extr b/Makefile.extr index f2d06def..b131e84b 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -43,7 +43,8 @@ cparser/pre_parser_messages.ml: DIRS=extraction \ lib common $(ARCH) backend cfrontend cparser driver \ - exportclight debug mppa_k1c/unittest mppa_k1c/abstractbb/Impure/ocaml + exportclight debug mppa_k1c/unittest mppa_k1c/abstractbb/Impure/ocaml \ + mppa_k1c/lib INCLUDES=$(patsubst %,-I %, $(DIRS)) -- cgit From 6e4f49f7b8154d21c2c42f9978e6829d7a22a1de Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 16 Sep 2020 07:52:57 +0200 Subject: starting to move common files --- Makefile.extr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.extr') diff --git a/Makefile.extr b/Makefile.extr index 59cc6c1d..5e328a4c 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -43,7 +43,7 @@ cparser/pre_parser_messages.ml: DIRS=extraction \ lib common $(ARCH) backend cfrontend cparser driver \ - exportclight debug kvx/unittest kvx/abstractbb/Impure/ocaml \ + exportclight debug kvx/unittest lib/Impure/ocaml \ kvx/lib INCLUDES=$(patsubst %,-I %, $(DIRS)) -- cgit From 93f9aa39b2885f98bf2be89583102d5c7f4c6f22 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 16 Sep 2020 09:13:59 +0200 Subject: just missing OpWeights for AARCH64 --- Makefile.extr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.extr') diff --git a/Makefile.extr b/Makefile.extr index 5e328a4c..1a894a16 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -42,7 +42,7 @@ cparser/pre_parser_messages.ml: # Directories containing plain Caml code DIRS=extraction \ - lib common $(ARCH) backend cfrontend cparser driver \ + lib common $(ARCH) scheduling backend cfrontend cparser driver \ exportclight debug kvx/unittest lib/Impure/ocaml \ kvx/lib -- cgit From 99d46d24e0282c3e4c5fe8765f4e755a1b3b0253 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 1 Oct 2020 10:42:22 +0200 Subject: ccomp.force target for forcing compilation without Coq processing --- Makefile.extr | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'Makefile.extr') 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) $+ -- cgit