Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374#!/bin/sh
# configure automatically sets up a wrapper at .git/hooks/pre-commit# which calls this script (if it exists).
set -e
dev/tools/check-overlays.sh
log=$(mktemp "git-fix-ws-log.XXXXXX")exec > "$log"
1>&2 echo "Auto fixing whitespace issues ($log)..."
# We fix whitespace in the index and in the working tree# separately to preserve non-added changes.index=$(mktemp "git-fix-ws-index.XXXXXX")fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXXX")tree=$(mktemp "git-fix-ws-tree.XXXXXX")echo "Patches are saved in '$index', '$fixed_index' and '$tree'."echo "If an error destroys your changes you can recover using them."echo "(The files are cleaned up on success.)"echo #newline
git diff-index -p --binary --cached HEAD > "$index"git diff-index -p --binary HEAD > "$tree"
# reset work tree and index# NB: untracked files which were not added are untouchedif [ -s "$index" ]; then git apply --whitespace=nowarn --cached -R "$index"; fiif [ -s "$tree" ]; then git apply --whitespace=nowarn -R "$tree"; fi
# Fix index# For end of file newlines we must go through the worktreeif [ -s "$index" ]; then echo "Fixing staged changes..." git apply --cached --whitespace=fix "$index" git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix git add -u echo #newlinefi
# reset work treegit diff-index -p --binary --cached HEAD > "$fixed_index"# If all changes were bad whitespace changes the patch is empty# making git fail. Don't fail now: we fix the worktree first.if [ -s "$fixed_index" ]; then git apply --whitespace=nowarn -R "$fixed_index"; fi
# Fix worktreeif [ -s "$tree" ]; then echo "Fixing unstaged changes..." git apply --whitespace=fix "$tree" git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix echo #newlinefi
if [ -s "$index" ] && ! [ -s "$fixed_index" ]; then echo "Fixing whitespace issues cancelled all changes." exit 1fi
# Check that we did fix whitespaceif ! git diff-index --check --cached HEAD; then echo "Auto-fixing whitespace failed: errors remain." echo "This may fix itself if you try again." echo "(Consider whether the number of errors decreases after each run.)" exit 1fiecho "Whitespace pass complete."
# clean up temporary filesrm "$index" "$tree" "$fixed_index" "$log"