diff options
Diffstat (limited to 'src/etc')
| -rwxr-xr-x | src/etc/pre-push.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/etc/pre-push.sh b/src/etc/pre-push.sh index a78725f2ab0..5f5b48bc1c0 100755 --- a/src/etc/pre-push.sh +++ b/src/etc/pre-push.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash # -# Call `tidy --bless` before each commit +# Call `tidy --bless` before git push # Copy this script to .git/hooks to activate, # and remove it from .git/hooks to deactivate. # @@ -14,6 +14,8 @@ COMMAND="$ROOT_DIR/x.py test tidy --bless" if [[ "$OSTYPE" == "msys" || "$OSTYPE" == "win32" ]]; then COMMAND="python $COMMAND" +elif ! command -v python &> /dev/null; then + COMMAND="python3 $COMMAND" fi echo "Running pre-push script '$COMMAND'" |