summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile10
1 files changed, 7 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index 47721ac5..2c324a41 100644
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,11 @@ ifeq (3.81,$(MAKE_VERSION))
install make, then invoke gmake instead of make)
endif
-all: build
+.PHONY: default
+default: build
+
+.PHONY: all
+all: build-test-verify nix
####################################
# Variables customizable by the user
@@ -67,7 +71,7 @@ build-bin-dir: build-driver build-lib
mkdir -p bin
cp -f compiler/_build/default/driver.exe bin/aeneas.exe
cp -f compiler/_build/default/driver.exe bin/aeneas.cmxs
- cp -rf fstar bin
+ cp -rf backends bin
.PHONY: doc
doc:
@@ -87,7 +91,7 @@ tests: trans-no_nested_borrows trans-paper \
# Verify the F* files generated by the translation
.PHONY: verify
-verify: build tests
+verify:
cd tests && $(MAKE) all
# Reformat the project