diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2019-10-13 14:50:16 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2019-10-13 14:50:16 -0400 |
| commit | 404429ca9197a508efc1be5425d6fc4a00a5eae9 (patch) | |
| tree | 88cfeb8b5334e0cb9bf9a7b991eeb741dfc9e9ee /lib | |
| parent | b71c7b9ec4580326772a212fbe011322ae1ac063 (diff) | |
Undo a questionable optimization, almost 10 years later (closes #179)
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions