Thomas Munro writes:
> As noted in a nearby review of some similar code[1], commit 7a2fe9bd
> made merge append very slightly more efficient, but nobody told
> cost_merge_append about the change. I doubt it makes much difference
> to the final cost in practice but I figured it might be worth
> co
Hi
As noted in a nearby review of some similar code[1], commit 7a2fe9bd
made merge append very slightly more efficient, but nobody told
cost_merge_append about the change. I doubt it makes much difference
to the final cost in practice but I figured it might be worth
correcting the comment. Does
