Skip to content
Fetching contributors…
Cannot retrieve contributors at this time
executable file 55 lines (41 sloc) 1.71 KB
echo command $1
case $1 in
echo "push libmscore upstream"
git subtree push -P libmscore master
echo "merge libmscore from upstream"
echo "permanently remove files"
set -o errexit
# Author: David Underhill
# Script to permanently delete files/folders from your git repository. To use
# it, cd to your repository's root and then run the script with a list of paths
# you want to delete, e.g., git-delete-history path1 path2
if [ $# -eq 0 ]; then
exit 0
# make sure we're at the root of git repo
if [ ! -d .git ]; then
echo "Error: must run this script from the root of a git repository"
exit 1
# remove all paths passed as arguments from the history of the repo
git filter-branch --index-filter "git rm -rf --cached --ignore-unmatch $files" HEAD
# remove the temporary history git-filter-branch otherwise leaves behind for a long time
rm -rf .git/refs/original/ && git reflog expire --all && git gc --aggressive --prune
git pull master
echo "gitpush -- push libmscore upstream"
echo "gitpull -- pull libmscore from upstream"
echo "gitremove a -- permanently remove file/folder a"
echo "gitupdate -- pull from master"
Something went wrong with that request. Please try again.