summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorSon Ho2022-09-22 18:46:28 +0200
committerSon Ho2022-09-22 18:46:28 +0200
commit0d5fb87166cc4eb4ddc783d871ad459479fc9fdc (patch)
treef8254c9590cc63846746b9751254c9b5951248c6 /Makefile
parent4a8b4b1be044ffaa8de72cf847c00184b6b8ab40 (diff)
Add a `format` target in the Makefile
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile5
1 files changed, 5 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 80cdad30..db308fbd 100644
--- a/Makefile
+++ b/Makefile
@@ -39,6 +39,11 @@ test: build trans-no_nested_borrows trans-paper \
verify: build test
cd tests && make all
+# Reformat the project
+.PHONY: format
+format:
+ dune build @fmt && dune promote
+
# Add specific options to some tests
trans-no_nested_borrows trans-paper: \
TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses