From bd0752cfdc4714a617881729c125f9ad27149ee2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 31 Oct 2019 13:07:59 +0100
Subject: [PATCH] don't pick up annotated copies in create_makefile.sh

---
 create_makefile.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/create_makefile.sh b/create_makefile.sh
index 5616e16da..8a7176c66 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -1,7 +1,7 @@
 #!/bin/bash 
 
 # options passed to `find` for locating relevant source files
-FIND_OPTS=( . -name '*.v' ! -name '*#*' ! -path './.git/*' )
+FIND_OPTS=( . -name '*.v' ! -name '*#*' ! -path './.git/*' ! -path './with-proof-state/*' )
 
 while ! [ -z "$1" ]
 do
-- 
GitLab