diff options
| author | Brendan Forster <brendan@github.com> | 2016-07-10 14:54:27 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-07-10 14:54:27 -0700 |
| commit | 00111374b47b684cb2196c9034ea92cbdfbf9c9f (patch) | |
| tree | 588aa9650ed151f3eb57129aa0673e469044bd27 /Agda.gitignore | |
| parent | 99dabe1835a69f1fb598084387ffa518aae75044 (diff) | |
| parent | 4616b76860f5a0e587cf63c3f12f2dd7631214d1 (diff) | |
| download | gitignore-00111374b47b684cb2196c9034ea92cbdfbf9c9f.tar.gz gitignore-00111374b47b684cb2196c9034ea92cbdfbf9c9f.zip | |
Merge pull request #2037 from koppor/patch-1
ignore busy indicator of uncompressed .synctex file
Diffstat (limited to 'Agda.gitignore')
0 files changed, 0 insertions, 0 deletions