`DocPreviewCleanup` workflow sometimes does not clean up previews

[sloede]

Right now, we have two documentation previews that were not deleted although the corresponding PR is not open anymore:

• [ ] #703 was merged
• [ ] #715 was closed but not merged

See also: https://github.com/trixi-framework/Trixi.jl/tree/d6e8fa39a754d24216232e14671c08d040fd7cf0/previews

Both points needs some investigating to find out what really is going on there.

[ranocha]

It looks like DocPreviewCleanup ran successfully for #703; https://github.com/trixi-framework/Trixi.jl/runs/3015705350?check_suite_focus=true. However, the preview is obviously still there...

• Time (cleanup action start): Thu, 08 Jul 2021 04:59:27 GMT
• Time (merge): Thu, 08 Jul 2021 06:59:16 GMT+2

Doesn't look suspicious to me...

[sloede]

Thanks for investigating! Thus, should the rule then be to

• either wait for the Documenter build to be finished before a merge, or
• if one closes a PR without merge, kill the Documenter action first

?

Would another possible solution be to modify the workflows to do this automatically? That is, on a pull request being closed (or merged), delete all currently running workflows for that PR? Or make the cleanup workflow depend on all (Documenter) workflows of a PR being finished?

[ranocha]

That sounds reasonable

[sloede]

Maybe something like this could be used: https://github.com/marketplace/actions/cancel-workflow-action#advanced-canceling-other-workflows

[sloede]

Xref: https://github.community/t/cancel-workflow-s-on-pr-being-closed-merged/189939