summaryrefslogtreecommitdiff
path: root/tests/fstar-split/Makefile
diff options
context:
space:
mode:
authorSon Ho2023-12-22 19:17:44 +0100
committerSon Ho2023-12-22 19:17:44 +0100
commit2171c01c6101958d3d12734ad970132b78d500d7 (patch)
treee79a75b12cbe7e1c3dff37727713fda722e0ad7f /tests/fstar-split/Makefile
parent29f358f4072ee4c6530b4c523a1754d4c0723893 (diff)
Start pushing files from the fstar-split test folder
Diffstat (limited to 'tests/fstar-split/Makefile')
-rw-r--r--tests/fstar-split/Makefile33
1 files changed, 33 insertions, 0 deletions
diff --git a/tests/fstar-split/Makefile b/tests/fstar-split/Makefile
new file mode 100644
index 00000000..6cf03386
--- /dev/null
+++ b/tests/fstar-split/Makefile
@@ -0,0 +1,33 @@
+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