I was doing some cleaning with some of my issues, branches, and branches of merged PR and remove a branch by mistake on the PR that @Eh2406 did based on my work on eager intersection of terms. It's reopened. Sorry for emails.
@Alex Tokarev do you still need the branch
I don't; it is just there as a reference. A local copy for me should be enough, so if you think it doesn't add any value I'll delete it.
ok, let's keep it if the reference can be useful for the time being
I've set up auto delete for merged branches to avoid future work.
Last updated: Oct 21 2021 at 21:02 UTC