aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2018-09-25 18:17:43 +0200
committerCyril SIX <cyril.six@kalray.eu>2018-09-25 18:17:43 +0200
commitfa5167f016145b5732b4da3c2aea26d808c63556 (patch)
tree8eabb2ad0e7fc119899d52a4ba576e3bed535970 /Makefile
parent589626969d7521b02db946e74736a0e2afe0dcb0 (diff)
downloadcompcert-kvx-fa5167f016145b5732b4da3c2aea26d808c63556.tar.gz
compcert-kvx-fa5167f016145b5732b4da3c2aea26d808c63556.zip
MB2AB - un peu d'avancement sur internal function
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index dbf034c2..4e189a91 100644
--- a/Makefile
+++ b/Makefile
@@ -96,7 +96,7 @@ BACKEND=\
Mach.v \
Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
Machblock.v Machblockgen.v Machblockgenproof.v \
- Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof.v \
+ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v \
Asmbundle.v Asmbundling.v Asmbundlingproof.v \
Asm.v Asmgen.v Asmgenproof.v