useful git stuff

gistfile1.txt

# ignore file permission changes
git config core.filemode false


http://joaquin.windmuller.ca/2011/11/16/selectively-select-changes-to-commit-with-git-or-imma-edit-your-hunk

https://web.archive.org/web/20170630184446/http://www.naleid.com/blog/2012/01/12/how-to-use-kdiff3-as-a-3-way-merge-tool-with-mercurial-git-and-tower-app/

http://blog.wuwon.id.au/2010/09/painless-merge-conflict-resolution-in.html

https://marcin-chwedczuk.github.io/use-meld-as-git-merge-diff-tool

https://martin-thoma.com/software-versioning-cheat-sheet/

https://git-scm.com/book/en/v2/Git-Tools-Rewriting-History

https://stackoverflow.com/questions/2428137/how-to-rebase-one-git-repository-onto-another-one

https://robots.thoughtbot.com/git-interactive-rebase-squash-amend-rewriting-history

https://stackoverflow.com/questions/11133290/which-version-of-the-git-file-will-be-finally-used-local-base-or-remote

https://gist.github.com/katylava/564416

Case sensitive search on github:
/(?-i)my_var/

To cherry pick-pick commits with a merge commit (to make the history look the same):

• create a new branch
• cherry pick the commits
• create a pull request
• merge

Since the pull request is merged via the Github web interface it uses the Name configured there (or github username if not configured), which may not match the name configured locally. To make it match:
git commit --amend --reset-author
git push --force

To uncommit last commit, after pushing it:
git reset HEAD~
git push --force
Note that if it hasn't been pushed, GitHub Desktop allows you to right-click and undo a commit, and then if you wish Repository>Discharge all changes