path: root/.github
diff options
authorSean Whitton <spwhitton@spwhitton.name>2018-12-31 18:14:54 +0000
committerSean Whitton <spwhitton@spwhitton.name>2018-12-31 18:14:54 +0000
commit4ebb8456547367f6d30115cab3d9e5c267cbc0ba (patch)
treefc28f85bc66fec9390510d82d21a8c490a137491 /.github
parent322f0f9659a54e8d2149ee51dac4843341274916 (diff)
add project administrivia files
Signed-off-by: Sean Whitton <spwhitton@spwhitton.name>
Diffstat (limited to '.github')
1 files changed, 13 insertions, 0 deletions
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
new file mode 100644
index 0000000..32cf2b6
--- /dev/null
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -0,0 +1,13 @@
+Thank you for your interest in contributing to this project!
+Please **do not** submit a pull request on GitHub. This repository is
+an automated mirror, and I don't develop using GitHub's platform.
+Instead, either
+- publish a branch somewhere (a GitHub fork is fine), and e-mail
+ <spwhitton@spwhitton.name> asking me to merge your branch, possibly
+ using git-request-pull(1)
+- prepare patches with git-format-patch(1), and send them to
+ <spwhitton@spwhitton.name>, possibly using git-send-email(1)