From 0c6e4e6e3cbf8187cf62bce64fb9b6e06a4036c6 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 28 Aug 2018 19:31:45 -0400
Subject: Mention dev/doc/critical-bugs in the PR template

---
 .github/PULL_REQUEST_TEMPLATE.md | 3 +++
 1 file changed, 3 insertions(+)

(limited to '.github')

diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index 4a8606a38a..f0747134da 100644
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -17,3 +17,6 @@ Fixes / closes #????
 <!-- (Otherwise, remove these lines.) -->
 - [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
 - [ ] Entry added in CHANGES.
+<!-- If this closes a critical bug (a proof of False): -->
+<!-- (Otherwise, remove this line.) -->
+- [ ] Corresponding entry in `dev/doc/critical-bugs` was added / updated
-- 
cgit v1.2.3