summaryrefslogtreecommitdiff
path: root/tests/Makefile.template
diff options
context:
space:
mode:
authorSon Ho2022-06-27 04:40:43 +0200
committerSon Ho2022-06-27 04:40:43 +0200
commit7f06278bd0b43426e88632afcd8e5633c5ab0a1e (patch)
treee0e7afef7d6bcc3cacf0dac40a0634f4a513a894 /tests/Makefile.template
parent3a930571516912714e3dcbc7ed1968228e593f99 (diff)
Update the Makefiles
Diffstat (limited to 'tests/Makefile.template')
-rw-r--r--tests/Makefile.template5
1 files changed, 1 insertions, 4 deletions
diff --git a/tests/Makefile.template b/tests/Makefile.template
index fed1a280..ea838d2d 100644
--- a/tests/Makefile.template
+++ b/tests/Makefile.template
@@ -21,10 +21,7 @@ ifeq (,$(filter %-in,$(MAKECMDGOALS)))
ifndef NODEPEND
ifndef MAKE_RESTARTS
.depend: .FORCE
- $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \
- --extract 'krml:*' \
- --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \
- > $@
+ $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@
.PHONY: .FORCE
.FORCE: