From 654326961d151dfff62a58aef8f16a00ed39b6b8 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 28 Jan 2020 02:32:41 +0100
Subject: docs: Add missing prefix (bug_*.v)

Related: https://github.com/coq/coq/pull/8630
---
 test-suite/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/README.md b/test-suite/README.md
index a2d5905710..96926f70b9 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -67,7 +67,7 @@ See [`test-suite/Makefile`](Makefile) for more information.
 ## Adding a test
 
 Regression tests for closed bugs should be added to
-[`bugs/closed`](bugs/closed), as `1234.v` where `1234` is the bug number.
+[`bugs/closed`](bugs/closed), as `bug_1234.v` where `1234` is the bug number.
 Files in this directory are tested for successful compilation.
 When you fix a bug, you should usually add a regression test here as well.
 
-- 
cgit v1.2.3