summaryrefslogtreecommitdiff
path: root/tests/fstar/Makefile
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/fstar/Makefile10
-rw-r--r--tests/fstar/Makefile.template3
2 files changed, 11 insertions, 2 deletions
diff --git a/tests/fstar/Makefile b/tests/fstar/Makefile
index a9c170f7..aad3354e 100644
--- a/tests/fstar/Makefile
+++ b/tests/fstar/Makefile
@@ -4,8 +4,10 @@ VERIFY_DIRS = $(addprefix verif-,$(ALL_DIRS))
CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS))
+COPY_MAKEFILES = $(addprefix copy-makefile-,$(ALL_DIRS))
+
.PHONY: all
-all: $(VERIFY_DIRS)
+all: $(COPY_MAKEFILES) $(VERIFY_DIRS)
.PHONY: clean
clean: $(CLEAN_DIRS)
@@ -14,6 +16,12 @@ clean: $(CLEAN_DIRS)
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-%:
cd $* && make clean
diff --git a/tests/fstar/Makefile.template b/tests/fstar/Makefile.template
index a16b0edb..14790d6d 100644
--- a/tests/fstar/Makefile.template
+++ b/tests/fstar/Makefile.template
@@ -8,7 +8,8 @@ FSTAR_OPTIONS = $(FSTAR_HINTS) \
--cache_checked_modules $(FSTAR_INCLUDES) --cmi \
--warn_error '+241@247+285-274' \
-FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
+FSTAR_EXE ?= fstar.exe
+FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)