User may want to skip tidy check sometimes

Author: chenyukang

src/etc/pre-push.sh

@@ -5,7 +5,7 @@
 # and remove it from .git/hooks to deactivate.
 #
 
-set -Eeuo pipefail
+set -Euo pipefail
 
 # https://github.com/rust-lang/rust/issues/77620#issuecomment-705144570
 unset GIT_DIR
@@ -15,3 +15,7 @@ echo "Running pre-push script $ROOT_DIR/x test tidy"
 
 cd "$ROOT_DIR"
 ./x test tidy --set build.locked-deps=true
+if [ $? -ne 0 ]; then
+    echo "You may use \`git push --no-verify\` to skip this check."
+    exit 1
+fi