etc/profile.d/git.sh

diff --git a/etc/profile.d/git.sh b/etc/profile.d/git.sh
index f191904e9d4a87adc97b65a2088b2c7f08916fb6..9f25dcd2a174414164dd8fcf982423c577675c80 100644 (file)
--- a/etc/profile.d/git.sh
+++ b/etc/profile.d/git.sh
@@ -27,7 +27,9 @@ git_log_files() {
        git log --pretty=format: --name-status
 }
 
-git_history_clean() {
+git_clean() {
+ git for-each-ref --format='delete %(refname)' refs/original | git update-ref --stdin
+ git reflog expire --expire=now --all
  git gc --prune=now --aggressive
 }
 
@@ -243,6 +245,15 @@ done
 )
 }
 
+git_push_origin() {
+       git push origin --force --all || return
+       git push origin --force --tags || return
+}
+
+git_rm_file() {
+       git filter-branch --force --index-filter "git rm --cached --ignore-unmatch $1" --prune-empty --tag-name-filter cat -- --all
+}
+
 # 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}
@@ -264,8 +275,7 @@ done
 # 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 --force --all || return
-# NB 12.01.18   git push origin --force --tags || return
+# NB 12.01.18   git_push_origin
 # NB 12.01.18 )
 # NB 12.01.18   rm -rf "$tmp"
 # NB 12.01.18 }