diff options
| author | Gaëtan Gilbert | 2020-11-10 16:52:51 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-16 11:25:07 +0100 |
| commit | bffa084eec75371c7df991c7a88aca5fe65114da (patch) | |
| tree | 451956c20e8c2213039e41b81df9232b0a41ef02 /dev/header.py | |
| parent | 779d2b915a970cdfc87d3d1b69e10bab04094f33 (diff) | |
Finish fixing setoid rewrite under anonymous lambdas (hopefully)
Fix #13246
Not sure if this is the right thing to do, but it seems to work.
Diffstat (limited to 'dev/header.py')
0 files changed, 0 insertions, 0 deletions