summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorJonathan Protzenko2022-02-17 15:54:05 -0800
committerJonathan Protzenko2022-02-17 15:54:05 -0800
commit9d1fc9e76ac82951c34952a878a36f7c5f886237 (patch)
tree752088e53849e874c85c770a0ada12b509235823 /Makefile
parent66a33c79cbb422377e706fedb7e62678498270bb (diff)
More stuff for the paper + interactive mode makefile
Diffstat (limited to '')
-rw-r--r--Makefile6
1 files changed, 3 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index 070aba6c..56847812 100644
--- a/Makefile
+++ b/Makefile
@@ -21,11 +21,11 @@ build:
# Test the project
.PHONY: test
-test: build translate-no_nested_borrows translate-hashmap
+test: build translate-no_nested_borrows translate-hashmap translate-paper
# Add specific options to some tests
-translate-no_nested_borrows: TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split -no-decreases-clauses
-translate-no_nested_borrows: SUBDIR:=misc
+translate-no_nested_borrows translate-paper: TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split -no-decreases-clauses
+translate-no_nested_borrows translate-paper: SUBDIR:=misc
translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses
translate-hashmap: SUBDIR:=hashmap