diff --git a/App/lib/lsp/LspServer.vp b/App/lib/lsp/LspServer.vp
index 82fba53..cc01e7c 100644
--- a/App/lib/lsp/LspServer.vp
+++ b/App/lib/lsp/LspServer.vp
@@ -36,6 +36,9 @@ _cancel_str: list[str]* = None
 # 1 when the client advertises pull diagnostics (`textDocument.diagnostic`). Pushing
 # publishDiagnostics as well would show every problem twice in the Problems panel.
 _pull_diagnostics: int = 0
+# The extension exposes `vipeye.disablePullDiagnostics`; when set, it must not advertise
+# diagnosticProvider at all (otherwise vscode-languageclient pulls regardless).
+_disable_pull_option: int = 0
 
 
 def _CancelAdd(pool: memhub.MemManager*, id_node: json.JsonValue*):
@@ -138,7 +141,7 @@ def _BuildInitializeResult(pool: memhub.MemManager*) -> json.JsonValue*:
     if sem is not None:
         json.object_set(pool, caps, "semanticTokensProvider", sem)
     diag: json.JsonValue* = json.object(pool)
-    if diag is not None:
+    if diag is not None and _disable_pull_option == 0:
         json.object_set(pool, diag, "interFileDependencies", json.bool_val(pool, False))
         json.object_set(pool, diag, "workspaceDiagnostics", json.bool_val(pool, False))
         json.object_set(pool, caps, "diagnosticProvider", diag)
@@ -166,8 +169,16 @@ def _ClientSupportsPull(params: json.JsonValue*) -> int:
 def _HandleInitialize(pool: memhub.MemManager*, tr: LspTransport.LspTransport*,
                       ws: LspWorkspace.LspWorkspace*, id_node: json.JsonValue*,
                       params: json.JsonValue*) -> int:
-    global _pull_diagnostics
-    _pull_diagnostics = _ClientSupportsPull(params)
+    global _pull_diagnostics, _disable_pull_option
+    init_opts: json.JsonValue* = None
+    if params is not None:
+        init_opts = params["initializationOptions"]
+    _disable_pull_option = 0
+    if init_opts is not None:
+        _disable_pull_option = LspRpc.GetIntField(init_opts, "disablePullDiagnostics", 0)
+    _pull_diagnostics = 0
+    if _disable_pull_option == 0:
+        _pull_diagnostics = _ClientSupportsPull(params)
     root_uri: str = None
     if params is not None:
         root_uri = LspRpc.GetStringField(params, "rootUri")
diff --git a/Tools/lsp/probe.py b/Tools/lsp/probe.py
index 826e4bc..f011ec1 100644
--- a/Tools/lsp/probe.py
+++ b/Tools/lsp/probe.py
@@ -481,6 +481,28 @@ def gate2(exe: str) -> int:
     pull_client.request("shutdown")
     pull_client.close()
 
+    # `vipeye.disablePullDiagnostics` must hide diagnosticProvider and fall back to push.
+    push_client = Client(exe)
+    init = push_client.request(
+        "initialize",
+        {"processId": os.getpid(), "rootUri": root.as_uri(),
+         "capabilities": {"textDocument": {"diagnostic": {}}},
+         "initializationOptions": {"disablePullDiagnostics": True}},
+    )
+    caps = init.get("result", {}).get("capabilities", {})
+    if "diagnosticProvider" in caps:
+        raise AssertionError(f"disablePullDiagnostics still advertises pull: {init}")
+    push_client.notify("initialized", {})
+    push_client.notify(
+        "textDocument/didOpen",
+        {"textDocument": {"uri": uri, "languageId": "viper", "version": 6, "text": overflow}},
+    )
+    publish = push_client.wait_notification("textDocument/publishDiagnostics")
+    if len(publish.get("params", {}).get("diagnostics", [])) != 1:
+        raise AssertionError(f"disablePullDiagnostics did not push: {publish}")
+    push_client.request("shutdown")
+    push_client.close()
+
     print("diagnostics: OK")
     print("recovery: OK")
     print("overflow-diagnostics: OK")