diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/external_revision_generator.py | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/scripts/external_revision_generator.py b/scripts/external_revision_generator.py index 493068ea..bdfe3549 100644 --- a/scripts/external_revision_generator.py +++ b/scripts/external_revision_generator.py @@ -33,7 +33,9 @@ if __name__ == '__main__': 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: |