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