diff options
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/Makefile | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/tests/fstar/Makefile b/tests/fstar/Makefile index aad3354e..6cf03386 100644 --- a/tests/fstar/Makefile +++ b/tests/fstar/Makefile @@ -7,10 +7,13 @@ CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS)) COPY_MAKEFILES = $(addprefix copy-makefile-,$(ALL_DIRS)) .PHONY: all -all: $(COPY_MAKEFILES) $(VERIFY_DIRS) +all: prepare-projects verify -.PHONY: clean -clean: $(CLEAN_DIRS) +.PHONY: prepare-projects +prepare-projects: $(COPY_MAKEFILES) + +.PHONY: verify +verify: $(VERIFY_DIRS) .PHONY: verif-% verif-%: @@ -22,6 +25,9 @@ copy-makefile-%: echo "# This file was automatically generated - modify ../Makefile.template instead" >> $*/Makefile cat Makefile.template >> $*/Makefile +.PHONY: clean +clean: $(CLEAN_DIRS) + .PHONY: clean-% clean-%: cd $* && make clean |