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