aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile.extr
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2019-01-11 17:32:20 +0100
committerCyril SIX <cyril.six@kalray.eu>2019-01-11 17:32:20 +0100
commita19cfffb026e8d0e26aeb366cdc9d76a04f459b6 (patch)
tree3d8cec869d4a7a57d40057793df7f462cd5e6945 /Makefile.extr
parent7d8199441bade8af697157658b6947bd0d9e94d0 (diff)
downloadcompcert-kvx-a19cfffb026e8d0e26aeb366cdc9d76a04f459b6.tar.gz
compcert-kvx-a19cfffb026e8d0e26aeb366cdc9d76a04f459b6.zip
Adding Mem as a possible location for accesses
Diffstat (limited to 'Makefile.extr')
-rw-r--r--Makefile.extr2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.extr b/Makefile.extr
index f5140a0c..3d54f61f 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -89,7 +89,7 @@ ifeq ($(wildcard .depend.extr),.depend.extr)
CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx)
ccomp: $(CCOMP_OBJS)
- @echo "Linking $@ with "$(CCOMP_OBJS)
+ @echo "Linking $@"
@$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+
ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo)