summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile7
1 files changed, 5 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 694dc964..aba2a67b 100644
--- a/Makefile
+++ b/Makefile
@@ -31,8 +31,8 @@ build:
.PHONY: test
test: build trans-no_nested_borrows trans-paper \
trans-hashmap trans-hashmap_main \
- trans-external trans-nll-betree_nll \
- trans-nll-betree_main
+ trans-external trans-constants \
+ trans-nll-betree_nll trans-nll-betree_main \
# Verify the F* files generated by the translation
.PHONY: verify
@@ -53,6 +53,9 @@ trans-hashmap_main: SUBDIR:=hashmap_on_disk
trans-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
trans-nll-betree_nll: SUBDIR:=misc
+trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
+trans-constants: SUBDIR:=misc
+
trans-external: TRANS_OPTIONS +=
trans-external: SUBDIR:=misc