diff options
author | Son Ho | 2024-02-09 17:23:57 +0100 |
---|---|---|
committer | Son Ho | 2024-02-09 17:23:57 +0100 |
commit | dd41ce4d968222824d36a295194a0de003d7a822 (patch) | |
tree | ab7c8d7dd3aa62e16e2cf84467da3d5fbb156711 /tests/fstar | |
parent | c285a3ff4fa6e7f8de182e574a7eb6d164cbee46 (diff) |
Remove a file which shouldn't have been added
Diffstat (limited to '')
-rw-r--r-- | tests/fstar-split/betree_back_stateful/Makefile | 49 |
1 files changed, 0 insertions, 49 deletions
diff --git a/tests/fstar-split/betree_back_stateful/Makefile b/tests/fstar-split/betree_back_stateful/Makefile deleted file mode 100644 index fa7d1f36..00000000 --- a/tests/fstar-split/betree_back_stateful/Makefile +++ /dev/null @@ -1,49 +0,0 @@ -# This file was automatically generated - modify ../Makefile.template instead -INCLUDE_DIRS = . - -FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) - -FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints - -FSTAR_OPTIONS = $(FSTAR_HINTS) \ - --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ - --warn_error '+241@247+285-274' \ - -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) - -# The F* roots are used to compute the dependency graph, and generate the .depend file -FSTAR_ROOTS ?= $(wildcard *.fst *.fsti) - -# Build all the files -all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS))) - -# This is the right way to ensure the .depend file always gets re-built. -ifeq (,$(filter %-in,$(MAKECMDGOALS))) -ifndef NODEPEND -ifndef MAKE_RESTARTS -.depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ - -.PHONY: .FORCE -.FORCE: -endif -endif - -include .depend -endif - -# For the interactive mode -%.fst-in %.fsti-in: - @echo $(FSTAR_OPTIONS) - -# Generete the .checked files in batch mode -%.checked: - $(FSTAR) $(FSTAR_OPTIONS) $< && \ - touch -c $@ - -.PHONY: clean -clean: - rm -f obj/* |