This is a simple copy of the current state of the .github on the develop branch, as of 2023-07-27. The stable branch .github dir should never be ahead of that on develop. Therefore this should be safe to do. Change-Id: I1e39de2d1f923d1834d0a77f79a1ff3220964bba