From 7c3b9842596f25ea8adc9e64f54a7785e4afaee2 Mon Sep 17 00:00:00 2001 From: HuStmpHrrr Date: Sat, 4 May 2024 12:40:24 -0400 Subject: [PATCH] fix scripts --- .github/scripts/check_projects.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/scripts/check_projects.sh b/.github/scripts/check_projects.sh index 1a401ed3..7062f415 100755 --- a/.github/scripts/check_projects.sh +++ b/.github/scripts/check_projects.sh @@ -10,7 +10,7 @@ error_out () { cd "${dir}" -for f in *.v; do +for f in `find -name '*.v'`; do grep -q -F "${f}" _CoqProject || error_out "${f}" done