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