If these jobs have the same name, GitHub allows merging a pull request
as soon as one of these jobs finishes.
We want to wait for all these jobs, so we have to use different names.
Since we don't skip this result job on [DOC], it's okay to use a
templated variable for this name.
Added by k0kubun (Takashi Kokubun) over 1 year ago
Use unique names for result jobs
If these jobs have the same name, GitHub allows merging a pull request
as soon as one of these jobs finishes.
We want to wait for all these jobs, so we have to use different names.
Since we don't skip this result job on [DOC], it's okay to use a
templated variable for this name.