From 541466263c1c673f9c4f762480b62b8f2648a920 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 19 Nov 2020 08:41:07 +0100 Subject: fix Makefile --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index ec28adf1..7d5b222c 100644 --- a/Makefile +++ b/Makefile @@ -122,7 +122,7 @@ BACKEND=\ Debugvar.v Debugvarproof.v \ Mach.v \ Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ - Asm.v Asmgen.v Asmgenproof.v Asmaux.v \ + Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v Asmaux.v \ $(BACKENDLIB) # C front-end modules (in cfrontend/) -- cgit