With #7802 recently merged, it would be nice to make docstub's output more visible in GitHub's UI. @stefanv suggested using the GITHUB_STEP_SUMMARY mechanism in #7802 (comment) (see also #7802 (comment)).

I haven't yet been able to figure out how to do that without masking the exit status and the output of docstub from the job log itself. If docstub returns a non-zero status the job should still fail and the job log should still contain all the details.