aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaxime Dénès2019-02-01 15:21:00 +0100
committerMaxime Dénès2019-02-01 15:21:00 +0100
commit506136d60c0dcc4fc2a2ca83ef3b586fbede55a2 (patch)
treebff71a590c0d23fa9a443d8efa1e7f8505588c75
parentaa2394d4ee6525b811db1e1eb58573c2f7aa749c (diff)
parentade9ef8200fcd0b40cf7369d9119f9aded7f1d5c (diff)
Merge PR #9415: Simplify the GitHub issue template
Ack-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares Ack-by: tchajed
-rw-r--r--.github/ISSUE_TEMPLATE.md21
1 files changed, 7 insertions, 14 deletions
diff --git a/.github/ISSUE_TEMPLATE.md b/.github/ISSUE_TEMPLATE.md
index c9cb516cd3..aec6cd0a21 100644
--- a/.github/ISSUE_TEMPLATE.md
+++ b/.github/ISSUE_TEMPLATE.md
@@ -1,18 +1,11 @@
-<!-- Thank you for your contribution.
- Please complete the following information when reporting a bug. -->
+<!-- Thank you for reporting a bug to Coq! -->
-#### Version
-
-<!-- You can get this information by running `coqtop -v`. -->
-
-
-#### Operating system
+#### Description of the problem
+<!-- If you can, it's helpful to provide self-contained example of some code
+that reproduces the bug. If not, a link to a larger example is also helpful. -->
-#### Description of the problem
+#### Coq Version
-<!-- It is helpful to provide enough information so that we can reproduce the bug.
- In particular, please include a code example which produces it.
- If the example is small, you can include it here between ``` ```.
- Otherwise, please provide a link to a repository, a gist (https://gist.github.com)
- or drag-and-drop a `.zip` archive. -->
+<!-- You can get this information by running `coqtop -v`. If relevant, please
+also include your operating system. -->