diff options
| author | Alec Theriault <alec.theriault@gmail.com> | 2018-12-17 09:25:10 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-17 09:25:10 -0500 |
| commit | ed43757aa371f9a532665783e27cff1703b4ac90 (patch) | |
| tree | d797068322124edcd022ebb1a2873a8b7157f0bf /.gitignore | |
| parent | 1380f7fa048ba26f79944452722dff0800b49038 (diff) | |
Refactor names + unused functions (#982)
This commit should not introduce any change in functionality!
* consistently use `getOccString` to convert `Name`s to strings
* compare names directly when possible (instead of comparing strings)
* get rid of unused utility functions
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions