From cc85a94027d1c60f274f3b5b9ead1aadafc2d333 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 11 Sep 2020 10:22:12 +0200
Subject: [PATCH] only check VFILES for options import

Fixes #345
---
 Makefile.coq.local | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile.coq.local b/Makefile.coq.local
index 4d618052e..3f5d3d828 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -13,7 +13,7 @@ NORMALIZER:=test-normalizer.sed
 
 test: $(TESTFILES:.v=.vo)
 # 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 \
 	done
 .PHONY: test
-- 
GitLab