From 293e792b47dc725f4e4ed4eb73dd47eef6ca04c5 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 19 Nov 2020 14:02:13 +0100
Subject: Asmgenproof1 pas sur kvx

---
 Makefile | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 7d5b222c..c126bfcb 100644
--- a/Makefile
+++ b/Makefile
@@ -122,9 +122,13 @@ BACKEND=\
   Debugvar.v Debugvarproof.v \
   Mach.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
-  Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v Asmaux.v \
+  Asm.v Asmgen.v Asmgenproof0.v Asmgenproof.v Asmaux.v \
   $(BACKENDLIB)
 
+ifneq ($(ARCH), "kvx")
+  BACKEND += Asmgenproof1.v 
+endif
+
 # C front-end modules (in cfrontend/)
 
 CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \
-- 
cgit