Cleanup

diff --git a/etc/profile.d/git.sh b/etc/profile.d/git.sh
index 588f81b14ee642f0cb286b3b425252790ab97914..f00b5cf3dd9c5589e0876bf41dc3b691437de8d6 100644 (file)
--- a/etc/profile.d/git.sh
+++ b/etc/profile.d/git.sh
@@ -280,29 +280,3 @@ git_purge_file() {
        git filter-branch --force --index-filter "git rm --cached --ignore-unmatch $1" --prune-empty --tag-name-filter cat -- --all
        echo "Now you can run git_push_origin"
 }
-
-# NB 12.01.18 git_clone_and_clean() {
-# NB 12.01.18   local usage="git_clean_repo REPO"
-# NB 12.01.18   local repo=${1:-?$usage}
-# NB 12.01.18   local tmp=/tmp/git_clone_and_clean.$$
-# NB 12.01.18 (
-# NB 12.01.18   rm -rf "$tmp"
-# NB 12.01.18   mkdir -p "$tmp"
-# NB 12.01.18   cd "$tmp" || return
-# NB 12.01.18   git_clone $repo . || return
-# NB 12.01.18   git_track_branches || return
-# NB 12.01.18 
-# NB 12.01.18   echo "Cleaning the files"
-# NB 12.01.18   git filter-branch --tag-name-filter cat --index-filter 'git rm -r --cached --ignore-unmatch filename' --prune-empty -f -- --all || return
-# NB 12.01.18 
-# NB 12.01.18   echo "Reclaim space"
-# NB 12.01.18   rm -rf .git/refs/original/ || return
-# NB 12.01.18   git reflog expire --expire=now --all || return
-# NB 12.01.18   git gc --prune=now || return
-# NB 12.01.18   git gc --aggressive --prune=now || return
-# NB 12.01.18 
-# NB 12.01.18   echo "Push the cleaned repository"
-# NB 12.01.18   git_push_origin
-# NB 12.01.18 )
-# NB 12.01.18   rm -rf "$tmp"
-# NB 12.01.18 }