Implement proper git SHA ID marking for builds during pull-requests (#1772)

* debug github CI git meta info

* fix push.yml format

* fix push.yml for shell

* try to fix push.yml

* try to fix push.yml run

* try to fix push.yml run for multi

* keep debugging

* try to do as less changes as possible

* Implement proper git tagging for builds during pull-requests

* Unify new-line separators between build steps

* Keep debugging

* make_translation.py: fix formatting

* push.yml: try to set ENV values

* push.yml: fix copy-paste error

* Remove extra env var

* Experimenting

* Testing upper()

* Re-testing upper()

* Revert tested values

* make_translation.py: add new lines between blocks to improve readability

* Reformulate docs & comments

* make_translation.py: remove debugging print

* make_translation.py: simplify check for SHA ID env var / code review

* make_translation.py: fix condition

---------

Co-authored-by: Ben V. Brown <5425387+Ralim@users.noreply.github.com>

Translations/make_translation.py

@@ -1264,7 +1264,14 @@ def get_translation_sanity_checks_text(defs: dict) -> str:
 
 
 def get_version_suffix(ver) -> str:
+    # Check env var from push.yml first:
+    # - if it's pull request then use vX.YY + C.ID for version line as in *C*I with proper tag instead of merge tag for detached tree
+    if os.environ.get("GITHUB_CI_PR_SHA", "") != "":
+        return "C" + "." + os.environ["GITHUB_CI_PR_SHA"][:8].upper()
+    # - no github PR SHA ID, hence keep checking
+
     suffix = str("")
+
     try:
         # Use commands _hoping_ they won't be too new for one environments nor deprecated for another ones:
         ## - get commit id; --short=8 - the shorted hash with 8 digits (increase/decrease if needed!)
@@ -1299,9 +1306,11 @@ def get_version_suffix(ver) -> str:
     except OSError:
         # Something _special_?
         suffix = "S"
+
     if "" == suffix:
         # Something _very_ special!
         suffix = "V"
+
     return suffix