summaryrefslogtreecommitdiff
path: root/.github
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2020-02-11 09:36:01 -0800
committerGitHub <noreply@github.com>2020-02-11 09:36:01 -0800
commit31930926314011d25ee0836bc690d37f9d3d360f (patch)
tree54164e9b73e97a6fbcfe4e1d667362d4447fc36f /.github
parent36f4f6b75bd13b7770e6113ed5c2f9b2b895e0ba (diff)
Update issue templates
Diffstat (limited to '.github')
-rw-r--r--.github/ISSUE_TEMPLATE/bug_report.md21
1 files changed, 21 insertions, 0 deletions
diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md
new file mode 100644
index 000000000..4b03c4e9f
--- /dev/null
+++ b/.github/ISSUE_TEMPLATE/bug_report.md
@@ -0,0 +1,21 @@
+---
+name: Bug report
+about: Create a report to help us improve
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Describe the bug**
+A clear and concise description of what the bug is.
+
+**Command line arguments**: Command line arguments passed to CVC4 if applicable
+**CVC4 version/commit**: Paste CVC4 version/commit here.
+**Operating system**: Name/version of the operating system.
+
+**`configure.sh` options**
+Paste `configure.sh` here.
+
+**`configure.sh` output**
+Paste the output of `configure.sh` here.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback