Skip to content

Commit

Permalink
Remove index.agda file after each verify.sh run
Browse files Browse the repository at this point in the history
  • Loading branch information
anfelor committed Apr 17, 2018
1 parent 41ce226 commit a6b88e4
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 1 deletion.
1 change: 0 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
@@ -1,2 +1 @@
*.agdai
index.agda
1 change: 1 addition & 0 deletions verify.sh
Original file line number Diff line number Diff line change
Expand Up @@ -4,3 +4,4 @@ for i in $( find src -name "*.agda" | sed 's/src\/\(.*\)\.agda/\1/' | sed 's/\//
echo "import $i" >> index.agda;
done;
agda -i . -i src/ index.agda
rm -rf index.agda;

0 comments on commit a6b88e4

Please sign in to comment.