summaryrefslogtreecommitdiffstats
path: root/options/gitignore/Agda
Commit message (Expand)AuthorAgeFilesLines
* chore: update gitignore list (#9437)Antoine GIRARD2019-12-191-0/+1
* Bindata is optional and over-writable on restart (#354)Thomas Boerger2016-12-221-0/+1