GitHub will go down in flames, don't use it!

Programming > Git >

(on Wikipedia)
https://github.com/

A website for hosting Git repositories.

I host a number of projects on GitHub, including:

• shell-random (shell-random on GitHub)

• misc-configuration on GitHub

• Prout -- Tells you when your pull-requests are live. Tells you when they're not, and should be.

--

• Relative Links in Pull Requests
• Placeholder for branch name in readme.md file

• https://web.archive.org/web/20221019050307/https://gitpop2.herokuapp.com/

  • Gives a better listing of a project's forks.
  • https://github.com/AndreMiras/gitpop2

Random usage notes ∞

• https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/proposing-changes-to-your-work-with-pull-requests/about-pull-requests  ^{[ 1 ]   [ 2 ]   [ 3 ]   [ 4 ]   [ 5 ]} 

Collapsible contents (code block) in comments / spoiler ∞

Collapsible contents (code block) in comments / spoiler tag #166

<details>
 <summary>Click to expand</summary>

```
your code block goes here
```
</details>

Do note the blank space between the summary tag and the backticks.

Change from SSH to https ∞

Smart HTTP Support will fix any ancient repositories which haven't been used in a while.

\git  remote  set-url  origin  https://github.com/YOURNAME/REPOSITORY.git

You may need to edit .git/config to change this section to be:

[branch "master"]
	remote = origin
	merge = refs/heads/master

Finding an email address ∞

You can look into the repository's log git log and might find an email in there.

Otherwise:

• https://stackoverflow.com/questions/12686545/how-to-leave-a-message-for-a-github-com-user

• https://www.sourcecon.com/how-to-find-almost-any-github-users-email-address/

1. Find the GitHub username for which you want the email.

2. Visit https://api.github.com/users/xxxxxxx/events/public

   • Change xxxxxxx to the person's GitHub username.

3. Press control f and search for "email".

or:

<input id=username type="text" placeholder="github username or repo link">
<button onclick="fetch(`https://api.github.com/users/${username.value.replace(/^.*com[/]([^/]*).*$/,'$1')}/events/public`).then(e=> e.json()).then(e => [...new Set([].concat.apply([],e.filter(x => x.type==='PushEvent').map(x => x.payload.commits.map(c => c.author.email)))).values()]).then(x => results.innerText = x)">GO</button>
<div id=results></div>

Fix WARNING: REMOTE HOST IDENTIFICATION HAS CHANGED! ∞

https://github.blog/2023-03-23-we-updated-our-rsa-ssh-host-key/

\ssh-keygen  -R github.com
\curl  -L https://api.github.com/meta  |\
  \jq  -r '.ssh_keys | .[]'  |\
  \sed  -e 's/^/github.com /'  >>  ~/.ssh/known_hosts

Footnotes

1. was https://docs.github.com/en/github/collaborating-with-pull-requests/proposing-changes-to-your-work-with-pull-requests/about-pull-requests - [↩]
2. was https://docs.github.com/en/github/collaborating-with-issues-and-pull-requests/proposing-changes-to-your-work-with-pull-requests/about-pull-requests - [↩]
3. was https://docs.github.com/en/github/collaborating-with-issues-and-pull-requests/about-pull-requests - [↩]
4. was https://docs.github.com/en/free-pro-team@latest/github/collaborating-with-issues-and-pull-requests/about-pull-requests - [↩]
5. was https://help.github.com/en/github/collaborating-with-issues-and-pull-requests/about-pull-requests - [↩]