From ada4195834f95b79c0b6f23a4ab8adc0618c6020 Mon Sep 17 00:00:00 2001 From: Aleksandar Markovic Date: Sat, 16 Apr 2022 18:30:35 +0200 Subject: [PATCH] doc: Move subsection on "Stale" label to the right place Label "Stale" is used for both issues and pull requests. It is currenly listed as applicaple to pull requests only, however. Move it to the right place. Signed-off-by: Aleksandar Markovic --- doc/project/dev_env_and_tools.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/project/dev_env_and_tools.rst b/doc/project/dev_env_and_tools.rst index 45c2f375279..83d6513b32c 100644 --- a/doc/project/dev_env_and_tools.rst +++ b/doc/project/dev_env_and_tools.rst @@ -331,10 +331,6 @@ to ensure proper review. See :ref:`review process `. This PR should not be merged (Do Not Merge). For work in progress, GitHub "draft" PRs are preferred. -* *Stale* - -PR which seems abandoned, and requires attention by the author. - * *Needs review* The PR needs attention from the maintainers. @@ -393,6 +389,10 @@ address an issue. Blocked by another PR or issue. +* *Stale* + +An issue or a PR which seems abandoned, and requires attention by the author. + * *In progress* For PRs: is work in progress and should not be merged yet. For issues: Is being