eeva/home-manager
1
0
Fork 0
mirror of https://github.com/nix-community/home-manager synced 2025-01-11 11:39:49 +01:00
Code Issues Releases Wiki Activity

github: copyedit stale bot's messages (#2658)

Browse source
This commit is contained in:
ash 2022-01-22 13:25:13 +00:00 committed by GitHub
parent 7eb5106548
commit e8a68de7ab
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
.github/stale.yml vendored
View file

@ -36,11 +36,11 @@ issues:
<details> <details>
<summary><b>Memorandum on closing issues</b></summary> <summary><b>Memorandum on closing issues</b></summary>
<p> <p>
If you have nothing of substance to add, please refrain from commenting and allow the bot close the issue. If you have nothing of substance to add, please refrain from commenting and allow the bot to close the issue.
Also, don't be afraid to manually close an issue, even if it holds valuable information. Also, don't be afraid to manually close an issue, even if it holds valuable information.
</p> </p>
<p> <p>
Closed issues stay in the system for people to search, read, cross-reference, or even reopen--nothing is lost! Closed issues stay in the system for people to search, read, cross-reference, or even reopen – nothing is lost!
Closing obsolete issues is an important way to help maintainers focus their time and effort. Closing obsolete issues is an important way to help maintainers focus their time and effort.
</p> </p>
</details> </details>
@ -57,7 +57,7 @@ pulls:
<summary><b>If you are the original author of the PR</b></summary> <summary><b>If you are the original author of the PR</b></summary>
<p> <p>
* GitHub sometimes doesn't notify people who commented / reviewed a PR previously, when you (force) push commits. *If you have addressed the reviews* you can [officially ask for a review](https://docs.github.com/en/github/collaborating-with-issues-and-pull-requests/requesting-a-pull-request-review) from those who commented to you or anyone else. * GitHub sometimes doesn't notify people who commented / reviewed a PR previously when you (force) push commits. *If you have addressed the reviews* you can [officially ask for a review](https://docs.github.com/en/github/collaborating-with-issues-and-pull-requests/requesting-a-pull-request-review) from those who commented to you or anyone else.
* If it is unfinished but you plan to finish it, please mark it as a draft. * If it is unfinished but you plan to finish it, please mark it as a draft.
* If you don't expect to work on it any time soon, please consider closing it with a short comment encouraging someone else to pick up your work. * If you don't expect to work on it any time soon, please consider closing it with a short comment encouraging someone else to pick up your work.
* To get things rolling again, rebase the PR against the target branch and address valid comments. * To get things rolling again, rebase the PR against the target branch and address valid comments.
@ -66,7 +66,7 @@ pulls:
</details> </details>
<details> <details>
<summary><b>If you are <i>not</i> the original author of the issue</b></summary> <summary><b>If you are <i>not</i> the original author of the PR</b></summary>
<p> <p>
* If you want to pick up the work on this PR, please create a new PR and indicate that it supercedes and closes this PR. * If you want to pick up the work on this PR, please create a new PR and indicate that it supercedes and closes this PR.