aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-04-10 16:41:34 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2019-04-11 11:01:29 -0400
commit60520cd8d08f63337225c0a2938827e00a2c48a3 (patch)
treeaaf3a2a7b75aabc1dee784c49da868907f4a1b54 /Makefile
parentbe2789ada63a1a5a6710da1abc73430f9b676399 (diff)
sed s'/RewriterProofs/RewriterAll/g'
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 42556fcf3..17d57cb07 100644
--- a/Makefile
+++ b/Makefile
@@ -51,7 +51,7 @@ LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \
src/RewriterWf1.vo \
src/RewriterWf2.vo \
src/RewriterRulesGood.vo \
- src/RewriterProofs.vo
+ src/RewriterAll.vo
NOBIGMEM_UNMADE_VOFILES := \
src/Curves/Weierstrass/AffineProofs.vo \
src/Curves/Weierstrass/Jacobian.vo \