Manually running CI jobs dist-various-{1,2} complains about missing metrics.json

[pjhades]

I ran the CI jobs dist-various-{1,2} manually by editing src/ci/github-actions/ci.yml but the jobs failed with the following error:

cp: cannot stat 'obj/build/metrics.json': No such file or directory

However I didn't touch anything on metrics. If I understand correctly, the cause of this error is:

• Build metrics were not enabled, because GITHUB_REF=refs/pull/111626/merge was defined in the environment, according to this logic.
• Build artifacts were asked to be uploaded, because DEPLOY=1 was defined in the environment, according to this logic.

I only ran dist-various-{1,2} but I guess that if other dist-* jobs are run manually, the same error would happen, because these jobs would have DEPLOY=1 or DEPLOY_ALT=1 but metrics would not be enabled as GITHUB_REF would be refs/pull/<PULL_REQUEST_ID>/merge.

I think this is somewhat confusing to people who want to use CI to test their PRs, because without this error their PRs could have passed the CI. I'm not sure what would be a good fix for this, maybe we could define an environment variable when build metrics are enabled, and check this variable before we fetch metrics.json. Or at least the problem could be mentioned in the document.