Git & CI#

Undo last commit without losing changes#

git reset HEAD~1 --soft

Running precommit hooks on files changed in the PR#

alias pc="git diff --name-only --diff-filter ACMR origin/master...HEAD | xargs pre-commit run --files"

GIT#

AIO discard, checkout master, prune etc#

git reset --hard HEAD && git checkout master && git pull && git gc --prune=now && git repack -Ad && git prune

Discard changes or stash#

git reset --hard HEAD

or

git stash --include-untracked
...later...
git pop

Permanently ignore changes on a file#

In some cases we don’t want to gitignore a file. This can happen if you work with multiple people, and an IDE extension always creates a file. The file creation is only happenning to you, and you don’t want to add too much pollution in the gitignore.

In this case, you can permanently ignore the change of a file with the following snippet

git update-index --assume-unchanged FILE

OR, edit .git/info/exclude and add the path of the excluded file.

Pushing to both Github and Huggingface#

git remote add origin git@(...).git
git remote set-url --push origin git@(...).git
git remote set-url --add --push origin https://{user}:{token}@huggingface.co/spaces/{user}/{space}
git remote -v
git push --set-upstream origin main

Purge and clean local .git folder#

git gc --prune=now
git repack -Ad
git prune
git gc --prune=now && git repack -Ad && git prune

Check sanity of local repo#

git gc --prune=now

Removing untracked files#

for dry run use -n parameter

Remove EVERY untracked file (including gitignored)#

git clean -fdx

Remove untracked file (but keep gitignored)#

git clean -fd

Remove untracked files (only gitignored ones)#

git clean -fdX