diff --git a/doc/examples/test_single.sh b/doc/examples/test_single.sh
index 8ca4f4d2f7..4138ee78a8 100755
--- a/doc/examples/test_single.sh
+++ b/doc/examples/test_single.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../tests/common.sh
 
-exec_check lean -j 0 "$f"
+exec_check lean -j 0 -Dlinter.nolint=true "$f"
diff --git a/tests/compiler/test_single_interpret.sh b/tests/compiler/test_single_interpret.sh
index dad72b7bf8..62ea05aa60 100755
--- a/tests/compiler/test_single_interpret.sh
+++ b/tests/compiler/test_single_interpret.sh
@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
 source ../common.sh
 
-exec_check lean --run "$f"
+exec_check lean -Dlinter.nolint=true --run "$f"
 diff_produced
diff --git a/tests/lean/interactive/test_single.sh b/tests/lean/interactive/test_single.sh
index ef2315c1cb..aa90be29df 100755
--- a/tests/lean/interactive/test_single.sh
+++ b/tests/lean/interactive/test_single.sh
@@ -6,5 +6,5 @@ source ../../common.sh
 export ASAN_OPTIONS=detect_leaks=0
 
 # these tests don't have to succeed
-exec_capture lean --run run.lean "$f" || true
+exec_capture lean -Dlinter.nolint=true --run run.lean "$f" || true
 diff_produced
diff --git a/tests/lean/run/test_single.sh b/tests/lean/run/test_single.sh
index bb152166f6..f8b89b49cc 100755
--- a/tests/lean/run/test_single.sh
+++ b/tests/lean/run/test_single.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../common.sh
 
-exec_check lean -j 0 "$f"
+exec_check lean -j 0 -Dlinter.nolint=true "$f"
diff --git a/tests/lean/server/diags.lean b/tests/lean/server/diags.lean
index 64e50227f6..e5d9677062 100644
--- a/tests/lean/server/diags.lean
+++ b/tests/lean/server/diags.lean
@@ -2,7 +2,7 @@ import Lean.Data.Lsp
 open IO Lean Lsp
 
 def main : IO Unit := do
-  Ipc.runWith (←IO.appPath) #["--server"] do
+  Ipc.runWith (←IO.appPath) #["--server", "-Dlinter.nolint=true"] do
     let hIn ← Ipc.stdin
     hIn.write (←FS.readBinFile "init_vscode_1_47_2.log")
     hIn.flush
diff --git a/tests/lean/server/test_single.sh b/tests/lean/server/test_single.sh
index d44dfb1e03..f4d0030dfb 100755
--- a/tests/lean/server/test_single.sh
+++ b/tests/lean/server/test_single.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../common.sh
 
-exec_check lean -j 0 --run "$f"
+exec_check lean -j 0 -Dlinter.nolint=true --run "$f"
diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh
index f9171faec0..b3abc830c2 100755
--- a/tests/lean/test_single.sh
+++ b/tests/lean/test_single.sh
@@ -2,5 +2,5 @@
 source ../common.sh
 
 # these tests don't have to succeed
-exec_capture lean -DprintMessageEndPos=true "$f" || true
+exec_capture lean -DprintMessageEndPos=true -Dlinter.nolint=true "$f" || true
 diff_produced
diff --git a/tests/lean/trust0/test_single.sh b/tests/lean/trust0/test_single.sh
index 4d109aa5bc..1ca0a9d5a0 100755
--- a/tests/lean/trust0/test_single.sh
+++ b/tests/lean/trust0/test_single.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../common.sh
 
-exec_check lean -t0 "$f"
+exec_check lean -t0 -Dlinter.nolint=true "$f"
diff --git a/tests/plugin/test_single.sh b/tests/plugin/test_single.sh
index cc19e3b6da..ba47d460cc 100755
--- a/tests/plugin/test_single.sh
+++ b/tests/plugin/test_single.sh
@@ -3,5 +3,5 @@ source ../common.sh
 
 compile_lean -shared -o "${f%.lean}.so"
 expected_ret=1
-exec_check lean --plugin="${f%.lean}.so" "$f"
+exec_check lean -Dlinter.nolint=true --plugin="${f%.lean}.so" "$f"
 diff_produced