Add needsRefresh to lint source config (#13050)

GitOrigin-RevId: bc6880f87bc81c7f0f022268a4d070c267421c46
This commit is contained in:
Alf Eaton
2023-05-17 08:05:36 +00:00
committed by Copybot
parent c8a72e96d4
commit c7544531c1
2 changed files with 4 additions and 14 deletions
@@ -1,4 +1,4 @@
import { EditorView } from '@codemirror/view'
import { EditorView, ViewUpdate } from '@codemirror/view'
import { Diagnostic, linter, lintGutter } from '@codemirror/lint'
import {
Compartment,
@@ -36,6 +36,9 @@ export const lintSourceConfig = {
tooltipFilter() {
return []
},
needsRefresh(update: ViewUpdate) {
return update.selectionSet
},
}
const compileLogLintSource = () =>