aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2018-07-02 20:47:27 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2018-07-03 19:28:55 -0400
commit2a7c3b95ea4fe28a6c4cd1c5b12e3bdbb6b75204 (patch)
tree55dca989c79b3fedb11ed11afd7af6a7cad46ce8 /Makefile
parente122effad97d68aa5c5e0314f49ca57642a77f2c (diff)
Remove another thing from the lite target
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index f9d64ac83..2cb11476c 100644
--- a/Makefile
+++ b/Makefile
@@ -87,6 +87,7 @@ LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \
src/Specific/X25519/C32/fe%.vo \
src/Experiments/NewPipeline/Toplevel2.vo \
src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo \
+ src/Experiments/SimplyTypedArithmetic.vo \
$(SPECIFIC_GENERATED_VOFILES)
NOBIGMEM_UNMADE_VOFILES := \
src/Curves/Weierstrass/AffineProofs.vo \