search

TriBITSPub / TriBITS

TriBITS: Tribal Build, Integrate, and Test System,
http://tribits.org
Other
36 stars 47 forks source link

Fix: gitdist: dist-repo-status: Display tag or SHA1 instead of 'HEAD' (GITHUB DEFECT) #589

Closed bartlettroscoe closed 1 year ago

bartlettroscoe commented 1 year ago

There was a bug is the previous PR #587. See commit messages for details.

bartlettroscoe commented 1 year ago

NOTE: GitHub is showing the commits for this PR here with the top commit https://github.com/TriBITSPub/TriBITS/pull/589/commits/81789b05db0b6b77f0c5cda64188dceb2e767f62 showing:

image

But the top commit for the PR branch gitdist-head-tag-and-sha1-fix is https://github.com/TriBITSPub/TriBITS/commit/a9696ffba7822cd158d4b5b2ec6650835d0be088 showing:

image

This would appear to be a defect in GitHub. I pushed rebased/amended commits pretty close to each other and I think there must be a race condition in GitHub.

Let's hope GitHub is smart enough to merge the correct commits.

I think I am going to leave this PR and branch alone and create a new branch with a new PR to be save. And I will leave this PR to show the defect in GitHub.