scripts/index-filter.sh

   1 #!/bin/bash
   2
   3 set -e
   4 set -o pipefail
   5
   6 ${SCRIPTS}/rewrite-index.pl | GIT_INDEX_FILE=$GIT_INDEX_FILE.new git update-index --index-info
   7
   8 if [ -f "$GIT_INDEX_FILE.new" ] ; then
   9     mv "$GIT_INDEX_FILE.new" "$GIT_INDEX_FILE"
  10 else
  11     rm "$GIT_INDEX_FILE"
  12 fi
  13
  14 exit 0