aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
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
parent7d8199441bade8af697157658b6947bd0d9e94d0 (diff)
downloadcompcert-kvx-a19cfffb026e8d0e26aeb366cdc9d76a04f459b6.tar.gz
compcert-kvx-a19cfffb026e8d0e26aeb366cdc9d76a04f459b6.zip
Adding Mem as a possible location for accesses
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 4eebaa37..f2a18d3f 100644
--- a/Makefile
+++ b/Makefile
@@ -140,6 +140,7 @@ all:
$(MAKE) proof
$(MAKE) extraction
$(MAKE) ccomp
+ $(MAKE) ccomp.byte
ifeq ($(HAS_RUNTIME_LIB),true)
$(MAKE) runtime
endif