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

fdupress merged 1 commit into

mainEasyCrypt/easycrypt:mainfrom

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