From d52138bfa10d7467ad1053610fa364815755babc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 7 May 2019 17:09:22 +0200
Subject: [PATCH] fix Makefile creation to not pick up files ending in .v in
 .git

If one names a branch "something-something-file.v", then the current
script will find it in the .git directory and try to compile git's
branch description as a Coq file...
---
 create_makefile.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/create_makefile.sh b/create_makefile.sh
index 4b9635fa1..114e18e6d 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -10,7 +10,7 @@ fi
 
 # Compile all *.v files (except the ones that define the decidable equality). Those
 # are directly included in other files.
-coq_makefile -f _CoqProject $(find . -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" -print) -o Makefile
+coq_makefile -f _CoqProject $(find . -name "*.v"  ! -name "*#*" ! -name "*eqdec*.v" ! -path "./.git/*" -print) -o Makefile
 
 # Fix the 'make validate' command. It doesn't handle the library prefix properly
 # and cause clashes for files with the same name. This forces full filenames and
-- 
GitLab