From e14dd4974f0ebfeb07a302064cc2fc5cd615019d Mon Sep 17 00:00:00 2001 From: Matthias Date: Mon, 29 Jul 2019 20:32:28 +0200 Subject: [PATCH] Improve release documentation --- docs/developer.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/developer.md b/docs/developer.md index f58e0597d..f50625111 100644 --- a/docs/developer.md +++ b/docs/developer.md @@ -156,6 +156,8 @@ git log --oneline --no-decorate --no-merges master..develop ### Create github release / tag +Once the PR against master is merged (best right after merging): + * Use the button "Draft a new release" in the Github UI (subsection releases) * Use the version-number specified as tag. * Use "master" as reference (this step comes after the above PR is merged).