Skip to content
Snippets Groups Projects
Commit bd0752cf authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

don't pick up annotated copies in create_makefile.sh

parent 323c243a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
create_makefile.sh
+ 1
− 1
View file @ bd0752cf
#!/bin/bash #!/bin/bash
# options passed to `find` for locating relevant source files # 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" ] while ! [ -z "$1" ]
do do
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment