diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000000..ccf0839c6a --- /dev/null +++ b/.gitattributes @@ -0,0 +1 @@ +*.xml filter=dater diff --git a/expand_date b/expand_date new file mode 100755 index 0000000000..3ffa2eab8c --- /dev/null +++ b/expand_date @@ -0,0 +1,20 @@ +#!/usr/bin/env python3 + +from os import getcwd +from subprocess import check_output, DEVNULL +from sys import stdin, stdout, argv + +content = stdin.read() + +# To editors: +# The usage of FETCH_HEAD here is very tricky. This is only intended for +# the cron job running "git pull" periodically. Humans should NOT rely on +# this script at all. Do NOT add "dater" filter into your .git/config. +# For editors, just use `git log ${path}` to show the history of a file. +cmd = [ 'git', 'log', '-1', '--pretty=%ad', 'FETCH_HEAD', '--', argv[1] ] +try: + date = check_output(cmd, cwd = getcwd(), stderr=DEVNULL).decode().rstrip() + content = content.replace('$Date$', '$Date: %s$' % date) +except Exception: + pass +stdout.write(content)