diff --git a/create_makefile.sh b/create_makefile.sh index 5616e16da50e7cedbe00e173e07fe2471388cbfd..8a7176c66651a95e7d3d3c238a62ba187b28c35f 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