|
|
|
|
|
by lucb1e
1087 days ago
|
|
I understood the comment, but that's not what OP was testing. They were doing the commits via merging pull requests. Git has no concept of a pull request and no HTTP API. From the post: > The GitHub API has periodic issues merging/creating PRs. (I use PRs since that is more reliable than keeping a local master up to date via pulling at this point). |
|
You are confidently wrong. Git, including pull requests, was developed years before GitHub ever existed. GitHub borrowed the term from git. Pull requests originally (before GitHub) are requests sent via email that one developer pull changes from another.
https://www.git-scm.com/docs/git-request-pull
The request pull command has been part of git since 2005:
https://github.com/git/git/blob/master/git-request-pull.sh
GitHub launched in 2008.
> and no HTTP API
Also wrong:
https://git-scm.com/book/en/v2/Git-on-the-Server-Smart-HTTP
There is nothing GitHub does with respect to git that you cannot do locally.