[ci] make the documentation build immune to the git-maintenance race - #1139

[ci] make the documentation build immune to the git-maintenance race#1139

strub merged 1 commit into

mainEasyCrypt/easycrypt:mainfrom

ci-docs-git-maintenanceEasyCrypt/easycrypt:ci-docs-git-maintenanceCopy head branch name to clipboard