55 lines
1.8 KiB
Bash
Executable file
55 lines
1.8 KiB
Bash
Executable file
#!/bin/bash
|
|
|
|
echo command $1
|
|
|
|
case $1 in
|
|
gitpush)
|
|
echo "push libmscore upstream"
|
|
git subtree push -P libmscore git@github.com:wschweer/libmscore.git master
|
|
;;
|
|
|
|
gitpull)
|
|
echo "merge libmscore from upstream"
|
|
git subtree pull -P libmscore git@github.com:wschweer/libmscore.git master
|
|
;;
|
|
|
|
gitremove)
|
|
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
|
|
fi
|
|
|
|
# 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
|
|
fi
|
|
|
|
# remove all paths passed as arguments from the history of the repo
|
|
files=$@
|
|
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
|
|
;;
|
|
|
|
gitupdate)
|
|
git pull git@github.com:musescore/MuseScore.git 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"
|
|
;;
|
|
esac
|
|
|