diff options
| author | Gavin Mak <gavinmak@google.com> | 2025-07-17 17:54:22 +0000 |
|---|---|---|
| committer | LUCI <gerrit-scoped@luci-project-accounts.iam.gserviceaccount.com> | 2025-07-17 15:41:59 -0700 |
| commit | 74edacd8e54a11c9358421894a5fcce04b02c47d (patch) | |
| tree | b0fbefcd0a70dd1ef04feb2367bdca63639959ad /platform_utils.py | |
| parent | 5d95ba8d85e189c25195beae9431d5f6823e083a (diff) | |
| download | git-repo-74edacd8e54a11c9358421894a5fcce04b02c47d.tar.gz | |
project: Use plumbing commands to manage HEAD
Don't directly manipulate `.git/HEAD` since it bypasses Git's internal
state management.
Bug: 432200791
Change-Id: I1c9264bcf107d34574a82b60a22ea2c83792951b
Reviewed-on: https://gerrit-review.googlesource.com/c/git-repo/+/491841
Commit-Queue: Gavin Mak <gavinmak@google.com>
Reviewed-by: Scott Lee <ddoman@google.com>
Tested-by: Gavin Mak <gavinmak@google.com>
Diffstat (limited to 'platform_utils.py')
0 files changed, 0 insertions, 0 deletions