diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-10-23 20:01:15 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-10-25 13:02:36 -0400 |
| commit | 8e029978760d6de340d7144f20b1a98a1b291058 (patch) | |
| tree | 5e9fb956a2023424f867b2ef0cf850037e56fdbb /.gitignore | |
| parent | 071ac04c39f1a0355b036db045175c12cdfb301f (diff) | |
[travis] Always display the diff, but don't display _CoqProject
Because remove_autogenerated.sh updates _CoqProject, and we don't want
to see the churn from that.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions