diff --git a/doc/dev/testing.md b/doc/dev/testing.md
index ed2efc1bb5..abb11ef263 100644
--- a/doc/dev/testing.md
+++ b/doc/dev/testing.md
@@ -51,6 +51,10 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
   codes and do not check the expected output even though output is
   produced, it is ignored.
 
+  **Note:** Tests in this directory run with `-Dlinter.all=false` to reduce noise.
+  If your test needs to verify linter behavior (e.g., deprecation warnings),
+  explicitly enable the relevant linter with `set_option linter.<name> true`.
+
 - [`tests/lean/interactive`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/): are designed to test server requests at a
   given position in the input file. Each .lean file contains comments
   that indicate how to simulate a client request at that position.