build: add time stamp for git hook logging

This commit is contained in:
Sören Weber 2024-01-18 21:01:41 +01:00
parent 9c13f0b514
commit 82767b6557
No known key found for this signature in database
GPG key ID: BEC6D55545451B6D

View file

@ -13,8 +13,9 @@
# echo 'execute .githooks/pre-push.py' >> .githooks/hooks.log
# python3 .githooks/pre-push.py
import subprocess
from datetime import datetime
import re
import subprocess
# This hook is called with the following parameters:
# $1 -- Name of the remote to which the push is being done
@ -28,13 +29,14 @@ import re
# an "#" (which are work in progress).
def main():
time = datetime.now().strftime("%Y-%m-%d %H:%M:%S")
local_branch = subprocess.check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'], universal_newlines=True).strip()
wip_prefix = '^#\\d+(?:\\b.*)$'
if re.match(wip_prefix, local_branch):
print(f'The branch {local_branch} can not be pushed as it starts with a "#" which marks it as work in progress', file=open(".githooks/hooks.log", "a"))
print(f'{time}: The branch {local_branch} can not be pushed as it starts with a "#" which marks it as work in progress', file=open(".githooks/hooks.log", "a"))
print(f'The branch {local_branch} can not be pushed as it starts with a "#" which marks it as work in progress')
exit(1)
print(f'Pushing branch {local_branch}', file=open(".githooks/hooks.log", "a"))
print(f'{time}: Pushing branch {local_branch}', file=open(".githooks/hooks.log", "a"))
exit(0)
if __name__ == "__main__":