Commit 195f23ec authored by Ralf Jung's avatar Ralf Jung
Browse files

fix invoking our linter

parent 0437f130
......@@ -12,7 +12,7 @@ style: $(VFILES)
$(SHOW)"Performing some style checks..."
$(HIDE)for FILE in $(VFILES); do \
if ! fgrep -q 'From stdpp Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
./ "$$FILE"; \
./ "$$FILE" || exit 1; \
.PHONY: style
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment