diff options
| author | Pierre-Marie Pédrot | 2019-05-01 17:55:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-10 12:53:09 +0200 |
| commit | 1c4a11ee8b5b48b85911689e1bb93757359cdfca (patch) | |
| tree | 91ac3458b33ab108bb9d0e340f824fa205bc2149 /dev | |
| parent | 4f3c70ad2deb8382130972c513cb19f0974580a8 (diff) | |
Fast-path for reordering of a single closed variable.
Doesn't seem to matter in practice, but it doesn't hurt either.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions