diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-27 11:49:55 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-27 11:49:55 -0700 |
| commit | 68c13c34a3be9035769193512f794cf805550df4 (patch) | |
| tree | 1a04618e745fd368887a0942c3e2c1f6f7987be0 /.gitignore | |
| parent | 27aa3a1e358ca9281721e3a3f4137979d16aab7e (diff) | |
Update .gitignore
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/.gitignore b/.gitignore index 9028c237e..f88b441c8 100644 --- a/.gitignore +++ b/.gitignore @@ -1,11 +1,10 @@ -bedrock -fiat +.#* *~ *# -*.vo +*.aux *.d *.glob -*.aux -*.vio -Makefile.coq Makefile.bak +Makefile.coq +*.vio +*.vo |