diff options
| author |  Lubomir I. Ivanov <neolit123@gmail.com> | 2017-11-16 15:51:17 +0200 |
|---|---|---|
| committer |  Dirk Hohndel <dirk@hohndel.org> | 2017-11-16 11:32:58 -0800 |
| commit | adb0adb1d2ee8661283bf4d1f9246d65d8203244 (patch) | |
| tree | 425a6484830e4cf0670d989af4fc7c66e1e5fdbf /.github | |
| parent | 063aadd166db883d9195ca88bf0b74f8675c8d86 (diff) | |
| download | subsurface-adb0adb1d2ee8661283bf4d1f9246d65d8203244.tar.gz | |
github: update PR template with 'documentation-change'
Add a 'Documentation change' section to the PR body.
This instructs the PR submitter to edit the section
with notes for the team editing the documentation.
If a PR has such notes, a maintainer should then
apply the needs-documentation-change label, so
that the documentation team can easily filter
such PRs by label.
Suggested-by: Miika Turkia <miika.turkia@gmail.com>
Signed-off-by: Lubomir I. Ivanov <neolit123@gmail.com>
Diffstat (limited to '.github')
| -rw-r--r-- | .github/PULL_REQUEST_TEMPLATE.md | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index 2265e7df2..7ba3fe91f 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -30,5 +30,10 @@ <!-- Describe if this change needs a release note present in ReleaseNotes/ReleaseNotes.txt. --> <!-- Also, please make sure to update the ReleaseNotes/ReleaseNotes.txt file itself. --> +### Documentation change: +<!-- If this PR makes changes to user functionality, then the documentation has to be updated too. --> +<!-- Please, briefly outline here what has changed in terms of the user experience (UX). --> +<!-- If UX changes have been made, a maintainer should apply the 'needs-documentation-change' label. --> + ### Mentions: <!-- Mention users that you want to review your pull request with @<user-name>. Leave empty if not sure. --> |