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>
This commit is contained in:
Lubomir I. Ivanov 2017-11-16 15:51:17 +02:00 committed by Dirk Hohndel
parent 063aadd166
commit adb0adb1d2

View file

@ -30,5 +30,10 @@
<!-- Describe if this change needs a release note present in ReleaseNotes/ReleaseNotes.txt. --> <!-- 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. --> <!-- 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: ### Mentions:
<!-- Mention users that you want to review your pull request with @<user-name>. Leave empty if not sure. --> <!-- Mention users that you want to review your pull request with @<user-name>. Leave empty if not sure. -->