Markus Lehtonen ad042f92f5 scripts/update-gh-pages: only update docs if version has been released ... Only update documentation if the version has been released (i.e. a git tag corresponding the version we're updating exists) or it is for the master branch. Prevents us from pointing users to documentation of an unreleased version. Also updates github workflow to fetch full commit history (including tags) so that git describe works correctly.		2020-12-03 12:54:14 +02:00
..
ISSUE_TEMPLATE	docs: specify container image in config	2020-11-20 17:00:19 +02:00
workflows	scripts/update-gh-pages: only update docs if version has been released	2020-12-03 12:54:14 +02:00