aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-11-14 19:06:47 +0000
committerYann Herklotz <git@yannherklotz.com>2020-11-14 19:06:47 +0000
commit4c73dd1076d9ba5ce9df0b00844ad2d670e8f618 (patch)
tree3e7f073ca67bfb94cffe79f5032aeb1d9733b127 /Makefile
parent4201a38997543ceedad52f77b992dd8eb4a2ee5e (diff)
downloadvericert-4c73dd1076d9ba5ce9df0b00844ad2d670e8f618.tar.gz
vericert-4c73dd1076d9ba5ce9df0b00844ad2d670e8f618.zip
Update lu.c and update Makefile with extraction
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index ee111eb..f8a3328 100644
--- a/Makefile
+++ b/Makefile
@@ -33,7 +33,7 @@ all: lib/COMPCERTSTAMP
lib/COMPCERTSTAMP:
(cd lib/CompCert && ./configure --ignore-coq-version $(ARCH))
- $(MAKE) -C lib/CompCert
+ $(MAKE) extraction -C lib/CompCert
touch $@
install: