From 7fe8212d42e6dee2d117d15f9acbd4c3decfad13 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 29 Aug 2018 11:34:43 -0400
Subject: Move mention of dev/doc/critical-bugs to CONTRIBUTING

As per https://github.com/coq/coq/pull/8349#pullrequestreview-150456919
---
 .github/PULL_REQUEST_TEMPLATE.md | 3 ---
 1 file changed, 3 deletions(-)

(limited to '.github')

diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index f0747134da..4a8606a38a 100644
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -17,6 +17,3 @@ 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