diff options
author | Ben Gamari <ben@smart-cactus.org> | 2020-12-03 10:31:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-03 10:31:27 -0500 |
commit | ef0375d6dc3d786c48067ecd6b84a58130829acd (patch) | |
tree | 52d1b381c2a0160c82f9f662915a46b78bf9a159 /.gitignore | |
parent | 284c9a0c304faf9c186421a62da5d8b4dc73a8a2 (diff) | |
parent | b2f1aef40cf50cf08eb28f34a9af2b1f9155c2df (diff) |
Merge pull request #1257 from AndreasPK/wip/andreask/opt_dumps
Update for changes in GHC's Pretty
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions