scripts: Prefer git.bat on Windows.
Calling git.bat seems to work in every instance, whereas some
installations don't have access to "git" directly.
diff --git a/scripts/external_revision_generator.py b/scripts/external_revision_generator.py
index 493068e..bdfe354 100644
--- a/scripts/external_revision_generator.py
+++ b/scripts/external_revision_generator.py
@@ -33,7 +33,9 @@
output_header_file = sys.argv[3]
# Extract commit ID from the specified source directory
- commit_id = subprocess.check_output(["git", "rev-parse", "HEAD"], cwd=source_dir).decode('utf-8').strip()
+ # Call git.bat on Windows for compatiblity.
+ git_binary = "git.bat" if os == "nt" else "git"
+ commit_id = subprocess.check_output([git_binary, "rev-parse", "HEAD"], cwd=source_dir).decode('utf-8').strip()
# Write commit ID to output header file
with open(output_header_file, "w") as header_file: