tree 41b339a7af310b47d866d3aa4763765f0fc1744f
parent 851d3ff4de964bf5ac17b6578dfb2cecb5f89099
author Henner Zeller <h.zeller@acm.org> 1743351318 -0700
committer Henner Zeller <h.zeller@acm.org> 1743353132 -0700

Don't send diagnostic notifiacations by default.

These days, editors seem to mostly use the feature to actively request
diagnostics, so sending them as notification is just creating
unnecessary churn and possibly are shown twice.

Default off now, but can be enabled with `--push_diagnostic_notifications`

Issues #2164 #2376