diff options
Diffstat (limited to 'tests/fstar-split/Makefile')
| -rw-r--r-- | tests/fstar-split/Makefile | 33 |
1 files changed, 0 insertions, 33 deletions
diff --git a/tests/fstar-split/Makefile b/tests/fstar-split/Makefile deleted file mode 100644 index 6cf03386..00000000 --- a/tests/fstar-split/Makefile +++ /dev/null @@ -1,33 +0,0 @@ -ALL_DIRS ?= $(filter-out Makefile%, $(wildcard *)) - -VERIFY_DIRS = $(addprefix verif-,$(ALL_DIRS)) - -CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS)) - -COPY_MAKEFILES = $(addprefix copy-makefile-,$(ALL_DIRS)) - -.PHONY: all -all: prepare-projects verify - -.PHONY: prepare-projects -prepare-projects: $(COPY_MAKEFILES) - -.PHONY: verify -verify: $(VERIFY_DIRS) - -.PHONY: verif-% -verif-%: - cd $* && make all - -.PHONY: copy-makefile-% -copy-makefile-%: - rm -f $*/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 |