diff options
| author | Florian Diebold <[email protected]> | 2021-04-08 13:21:22 +0100 |
|---|---|---|
| committer | Florian Diebold <[email protected]> | 2021-04-08 13:23:17 +0100 |
| commit | 8040f4a5e3792f95b3194e21b3f6d375fb7499c5 (patch) | |
| tree | baf287e6d05568319662cd32d56ded5354edecd6 /editors/code | |
| parent | 8ce6fea325c001deeed2857da560fa5cfbc6eea3 (diff) | |
Replace `make_binders` by the now equivalent `make_only_type_binders`
Diffstat (limited to 'editors/code')
0 files changed, 0 insertions, 0 deletions