also who the heck decided it should be called pull request, that's the worst and most confusing possible name for it
@lizardsquid What it is is github doesn't give a single shit about usability
@lizardsquid
Isn't it really a request to push something
@DialMforMara yes
@lizardsquid agreed--but I assume GitHub took the name from the git request-pull subcommand, which exists to "Generate a request asking your upstream project to pull changes into their tree."
@lizardsquid I still don't know what it actually is because I've never tried looking.
@vudw other people have pointed out it's called a "merge request" in other things
it was accepted✨