diff options
| author | Gaëtan Gilbert | 2020-10-02 14:47:13 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-02 15:17:49 +0200 |
| commit | 0c1265f56a46e79aac85ae2c08cd6261141b0788 (patch) | |
| tree | 2958d8f20f59e02cc7d645567eb12ea3cce433f6 /doc/plugin_tutorial/tuto2 | |
| parent | d3b965cf054e6649bf9d058fae3e9645e3609649 (diff) | |
setoid_rewrite: record generated name when rewriting under lambda
Fix #13129
Diffstat (limited to 'doc/plugin_tutorial/tuto2')
0 files changed, 0 insertions, 0 deletions