Skip to content
Snippets Groups Projects
Commit cc85a940 authored by Ralf Jung's avatar Ralf Jung
Browse files

only check VFILES for options import

Fixes #345
parent 1520e6a5
No related branches found
No related tags found
No related merge requests found
...@@ -13,7 +13,7 @@ NORMALIZER:=test-normalizer.sed ...@@ -13,7 +13,7 @@ NORMALIZER:=test-normalizer.sed
test: $(TESTFILES:.v=.vo) test: $(TESTFILES:.v=.vo)
# Make sure everything imports the options. # Make sure everything imports the options.
$(HIDE)for FILE in $$(find theories/ -name "*.v" | fgrep -v theories/options.v); do \ $(HIDE)for FILE in $(filter-out theories/options.v,$(VFILES)); do \
if ! fgrep -q 'From iris Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; exit 1; fi \ if ! fgrep -q 'From iris Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; exit 1; fi \
done done
.PHONY: test .PHONY: test
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment