Implement proper git SHA ID marking for builds during pull-requests

[ia]

• Please check if the PR fulfills these requirements

• The changes have been tested locally
• There are no breaking changes

• What kind of change does this PR introduce?
  Implement proper git SHA ID marking for builds during pull-requests.

• What is the current behavior?
  If a build has been produced on github CI after creating pull request, then git SHA ID doesn't equal to the latest git SHA ID in a user's branch.

• What is the new behavior (if this is a feature change)?
  Retrieve proper git SHA ID for marking builds during pull-requests using github CI environment variables through push.yml features.

• Other information:
  As far as I understand (according to some pieces of information), here is what github does on builds for pull-requests:

• git checkout COMMIT-ID_from_user_branch
• git merge UPSTREAM
  Therefore, getting COMMIT_ID using git command returns SHA ID for merge commit and not the latest commit to user branch. But with a couple of tricks there is a way to get original SHA ID. I tried to make as less changes as possible. Documentation updated as well. Debugging print in make_translation will be removed once I double-check the output after creating this PR.

[ia]

To be fully clear since this is very confusing for myself. Here is what I'm talking about:

• the latest commit to my branch is 94d0fd7
• Pinecilv2_multi-lang build is properly marked now here
• before it would be something like that - getting branch goes to exception since it's in detached HEAD due to git checkout COMMIT_ID, hence current tagging would fall back to "homebrew" (however local but not github "detached HEAD" is a different case which I would like to address separately some time later)
• but even for this build if we go to metadata.zip here (there is the actual current SHA ID in JSONs), then it will be 7867043 and not 94d0fd7 because 7867043 is a merge SHA ID known to github ci only (I will fix this later as well).

Proper tagging never was so over-complicated for me before. Have no idea why it's not a github job to do it automagically for its users.

P.S. It's not like I'm obsessed with that much. But since git has commit IDs which let you to identify builds, then it's just super convenient when you have to deal with building & testing multiple builds from different sources on one device: after some time break instead of recalling what was the last flashed build, you can just go to debug menu and check SHA to verify. But only if it's properly tagged.

[ia]

Now I consider this ready for review. No rush, just letting you know. ;)

[Ralim]

I don't mind this, but also this is making the complexity of the hashing far more complex than it really ought to be. It's only there really as a means of checking if this was the release version or if this was a wip tag