Skip to content

Commit

Permalink
use --ext context_pruning with new Makefiles
Browse files Browse the repository at this point in the history
  • Loading branch information
tahina-pro committed Oct 25, 2024
1 parent 1b08afc commit 9b78c60
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/common.Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ FSTAR_OPTIONS += $(PROFILE)
FSTAR_FILES ?= $(wildcard $(addsuffix /*.fst,$(SRC_DIRS)) $(addsuffix /*.fsti,$(SRC_DIRS)))

# `ALREADY_CACHED` expected to be empty or to end with a comma
FSTAR_OPTIONS += $(OTHERFLAGS) $(addprefix --include ,$(INCLUDE_PATHS)) --cache_checked_modules --warn_error @241 --already_cached $(ALREADY_CACHED)Prims,FStar,LowStar --cmi
FSTAR_OPTIONS += $(OTHERFLAGS) $(addprefix --include ,$(INCLUDE_PATHS)) --cache_checked_modules --warn_error @241 --already_cached $(ALREADY_CACHED)Prims,FStar,LowStar --cmi --ext context_pruning

# Passing RESOURCEMONITOR=1 will create .runlim files through the source tree with
# information about the time and space taken by each F* invocation.
Expand Down

0 comments on commit 9b78c60

Please sign in to comment.