From 6e3162f92f0fc5ac88a946d001b3912fff9c999d Mon Sep 17 00:00:00 2001 From: Laurent Cozic Date: Sat, 2 Mar 2024 15:32:21 +0000 Subject: [PATCH] Tools: Always run all checks on CI --- .github/scripts/run_ci.sh | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/scripts/run_ci.sh b/.github/scripts/run_ci.sh index 6db4364ad..e4bb382fa 100755 --- a/.github/scripts/run_ci.sh +++ b/.github/scripts/run_ci.sh @@ -19,6 +19,12 @@ if [ "$GITHUB_EVENT_NAME" == "pull_request" ]; then IS_PULL_REQUEST=1 fi +# In some case it might not be possible to detect if we're on a pull request, for example when +# pushing new code to an existing code (or maybe when pressing "Update branch" from GitHub). In that +# case "GITHUB_EVENT_NAME" is "push" it's not clear what else could be checked. It seems safe to +# always run the checks anyway so we do this for now. +IS_PULL_REQUEST=1 + if [[ $GIT_TAG_NAME = $SERVER_TAG_PREFIX-* ]]; then IS_SERVER_RELEASE=1 fi