docs: add 'edit-on-github' link to html theme

Closes IDF-1504
This commit is contained in:
Marius Vikhammer
2020-05-06 17:25:23 +08:00
parent a97cd645ad
commit 214f1fbbed
3 changed files with 33 additions and 13 deletions

15
docs/get_github_rev.py Normal file
View File

@@ -0,0 +1,15 @@
import subprocess
# Get revision used for constructing github URLs
def get_github_rev():
path = subprocess.check_output(['git', 'rev-parse', '--short', 'HEAD']).strip().decode('utf-8')
try:
tag = subprocess.check_output(['git', 'describe', '--exact-match']).strip().decode('utf-8')
except subprocess.CalledProcessError:
tag = None
print('Git commit ID: ', path)
if tag:
print('Git tag: ', tag)
return tag
return path