File: pre-commit

package info (click to toggle)
coq-doc 8.16.1-1
  • links: PTS, VCS
  • area: non-free
  • in suites: bookworm
  • size: 42,788 kB
  • sloc: ml: 219,673; sh: 4,035; python: 3,372; ansic: 2,529; makefile: 728; lisp: 279; javascript: 87; xml: 24; sed: 2
file content (73 lines) | stat: -rwxr-xr-x 2,422 bytes parent folder | download | duplicates (4)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
#!/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 untouched
if [ -s "$index" ]; then git apply --whitespace=nowarn --cached -R "$index"; fi
if [ -s "$tree" ]; then git apply --whitespace=nowarn -R "$tree"; fi

# Fix index
# For end of file newlines we must go through the worktree
if [ -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 #newline
fi

# reset work tree
git 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 worktree
if [ -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 #newline
fi

if [ -s "$index" ] && ! [ -s "$fixed_index" ]; then
    echo "Fixing whitespace issues cancelled all changes."
    exit 1
fi

# Check that we did fix whitespace
if ! 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 1
fi
echo "Whitespace pass complete."

# clean up temporary files
rm "$index" "$tree" "$fixed_index" "$log"