diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2020-02-06 17:55:15 -0500 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2020-02-06 17:55:15 -0500 |
| commit | b0690cc786c858b4a41c7682937bebd53d318f6a (patch) | |
| tree | 24f36ba4a06ab465c185e93ac38959d663944cd0 /.gitignore | |
| parent | dbdf458dc49191a6f355a16bae839a2d618513b7 (diff) | |
| parent | 5ed96ea023de0570061660363ee55c3f9cffda18 (diff) | |
Merge pull request #196 from mdempsky/manual-edits
Manual edits
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions