summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-18 12:30:00 +0100
committerSon Ho2022-02-18 12:30:00 +0100
commit1fa2f2812215da74cb793dc63d621a8d15c55523 (patch)
tree3fe039b4e2e5338dbb4641e65e87172e5b09da28
parent68a91446114372478ad74a1e6113b842162e56c5 (diff)
parent9d1fc9e76ac82951c34952a878a36f7c5f886237 (diff)
Merge branch 'main' of github.com:Kachoc/aeneas into main
-rw-r--r--Makefile6
-rw-r--r--tests/misc/Makefile2
2 files changed, 5 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index c485ef48..5ae0ea4c 100644
--- a/Makefile
+++ b/Makefile
@@ -22,11 +22,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