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

fdupress wants to merge 1 commit into

docker-consolidateEasyCrypt/easycrypt:docker-consolidatefrom

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