github actions: workaround for ondrej/php apt repository update error#2143

nodiscc merged 1 commit into

shaarli:mastershaarli/Shaarli:masterfrom

nodiscc:fix-ci-php-updatenodiscc/Shaarli:fix-ci-php-updateCopy head branch name to clipboard