[ci] do not rebuild base in PR runs#1008

fdupress wants to merge 2 commits into

mainEasyCrypt/easycrypt:mainfrom

ci-retrieve-baseEasyCrypt/easycrypt:ci-retrieve-baseCopy head branch name to clipboard