feat: add linter.extra.dupNamespace.consecutiveOnly option to dupNamespace linter#14249

wkrozowski merged 3 commits into

leanprover:masterleanprover/lean4:masterfrom

wkrozowski:wojciech/dupNamespace_non_consecutivewkrozowski/lean4:wojciech/dupNamespace_non_consecutiveCopy head branch name to clipboard