diff --git a/.github/scripts/get_changed_php.sh b/.github/scripts/get_changed_php.sh index f6b8bbaf71d..192de878900 100755 --- a/.github/scripts/get_changed_php.sh +++ b/.github/scripts/get_changed_php.sh @@ -48,8 +48,11 @@ while true; do response=$(curl -s -H "Authorization: token ${GITHUB_TOKEN}" \ "https://api.github.com/repos/${owner}/${repo}/pulls/${pr_number}/files?per_page=${per_page}&page=${page}") + phan_exclude_file_regex=$(php -r '$config = require("dev/tools/phan/config.php"); echo $config["exclude_file_regex"];') + + # Filter for files ending with .php and add them to the list - mapfile -t files < <(echo "$response" | jq -r '.[] | select((.filename | test("\\.php$")) and (.filename | test("^dev/") | not)) | .filename') + mapfile -t files < <(echo "$response" | jq -r '.[] | select((.filename | test("\\.php$")) and (.filename | test("^dev/") | not)) | .filename' | grep -vP "$phan_exclude_file_regex") changed_php_files+=("${files[@]}") mapfile -t files < <(echo "$response" | jq -r '.[] | select(.filename | test("\\.lang$")) | .filename')