Skip to content

Users/pgo/push only diagnostics - #357

Merged
pgourlain merged 5 commits into
masterfrom
users/pgo/push-only-diagnostics
Sep 26, 2026
Merged

pgourlain merged 5 commits into
masterfrom
users/pgo/push-only-diagnostics

Conversation

@pgourlain

Copy link
Copy Markdown
Owner

#356 : Header files (.hrl) treated as modules

  • Opening a .hrl no longer reports no module definition and record ... is unused for every record it declares: the pull-diagnostics path (textDocument/diagnostic, workspace/diagnostic) linted any file on its own, unlike the push path which only ever lints .erl files. Both now lint .erl files only

Diagnostics are pushed only : due too many conflicts with pull/push for diagnostics, I keep only push

@pgourlain
pgourlain merged commit 641a575 into master Sep 26, 2026
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant