aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-22 08:12:41 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-22 08:12:41 +0100
commit5a425ba34f3f2520de752ea95a4636a9437c312a (patch)
tree91a1ef113e01f6e7a1006e8ef4e84e9d1f6bab04 /Makefile
parentba2b825a42807102a93cd6df1ce90b41d415569c (diff)
downloadcompcert-kvx-5a425ba34f3f2520de752ea95a4636a9437c312a.tar.gz
compcert-kvx-5a425ba34f3f2520de752ea95a4636a9437c312a.zip
ça recompile sur x86
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index ed9059db..d8cd428a 100644
--- a/Makefile
+++ b/Makefile
@@ -72,7 +72,7 @@ COMMON=Errors.v AST.v Linking.v \
# Back-end modules (in backend/, $(ARCH)/)
BACKEND=\
- Cminor.v Op.v CminorSel.v \
+ Cminor.v Op.v CminorSel.v OpHelpers.v OpHelpersproof.v \
SelectOp.v SelectDiv.v SplitLong.v SelectLong.v Selection.v \
SelectOpproof.v SelectDivproof.v SplitLongproof.v \
SelectLongproof.v Selectionproof.v \