aboutsummaryrefslogtreecommitdiff
path: root/editors/code
diff options
context:
space:
mode:
authorFlorian Diebold <[email protected]>2021-04-08 13:21:22 +0100
committerFlorian Diebold <[email protected]>2021-04-08 13:23:17 +0100
commit8040f4a5e3792f95b3194e21b3f6d375fb7499c5 (patch)
treebaf287e6d05568319662cd32d56ded5354edecd6 /editors/code
parent8ce6fea325c001deeed2857da560fa5cfbc6eea3 (diff)
Replace `make_binders` by the now equivalent `make_only_type_binders`
Diffstat (limited to 'editors/code')
0 files changed, 0 insertions, 0 deletions