Closed bartlettroscoe closed 1 year ago
There was a bug is the previous PR #587. See commit messages for details.
This replaces the following PR that seems to show a GitHub defect described in https://github.com/TriBITSPub/TriBITS/pull/589#issuecomment-1615052483:
I was afraid that the GitHub defect would cause the merge of the wrong commits.
There was a bug is the previous PR #587. See commit messages for details.
This replaces the following PR that seems to show a GitHub defect described in https://github.com/TriBITSPub/TriBITS/pull/589#issuecomment-1615052483:
589
I was afraid that the GitHub defect would cause the merge of the wrong commits.