summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile6
-rw-r--r--tests/misc/Makefile2
2 files changed, 5 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
diff --git a/tests/misc/Makefile b/tests/misc/Makefile
new file mode 100644
index 00000000..5153d201
--- /dev/null
+++ b/tests/misc/Makefile
@@ -0,0 +1,2 @@
+%.fst-in %.fsti-in:
+ @echo --include ../hashmap