From 5fc074e924a705baf6344bc4e0c0916bc1b6c542 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Mar 2021 15:03:43 +0100
Subject: Mention overlays in PR template

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

diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index 3bd3342329..df9e14b178 100644
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -17,3 +17,5 @@ Fixes / closes #????
 <!-- (Otherwise, remove these lines.) -->
 - [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
 - [ ] Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).
+- [ ] Overlay pull requests (if this breaks 3rd party developments in CI, see
+https://github.com/coq/coq/blob/master/dev/ci/user-overlays/README.md for details)
-- 
cgit v1.2.3