message: chore: no gutters on server failure
diff: @@ -86,7 +86,7 @@ export class LeanTaskGutter implements Disposable {
  if (editor.document.languageId !== 'lean4' && editor.document.languageId !== 'lean') continue;
  const uri = editor.document.uri.toString();
  uris[uri] = true
  - const processed = uri in this.status ? this.status[uri] : 0
  + const processed = uri in this.status ? this.status[uri] : undefined
  if (this.gutters[uri]) {
  this.gutters[uri].setProcessed(processed)
  } else {
  