Markus Lehtonen ef3ad8f5f3 github: prevent parallel runs of gh-pages update ... Ensure sequential updates to the gh-pages branch. Otherwise, if parallel jobs are triggered, onnly one (the first to complete) will succeed and the others will fail with git push error (because the tip of the gh-pages has moved and their commit doesn't apply anymore).		2023-09-15 11:43:23 +03:00
..
ISSUE_TEMPLATE	github: update assignees in new-release issue template	2023-07-21 09:06:42 +03:00
workflows	github: prevent parallel runs of gh-pages update	2023-09-15 11:43:23 +03:00