Code

Assorted test fixes#340

Code

Merged

mhuisi merged 6 commits intoleanprover:masterleanprover/vscode-lean4:masterfrom mhuisi:mhuisi/assorted-test-fixesmhuisi/vscode-lean4:mhuisi/assorted-test-fixesCopy head branch name to clipboardOct 19, 2023

+55-14

Commits

Commits on Oct 18, 2023

• lazily fill exports

  mhuisi

  committed
  c537caf

• test: wait for infoviewprovider

  mhuisi

  committed
  e14d04b

• test: don't show modal dialogs in tests

  mhuisi

  committed
  5cab99c

Commits on Oct 19, 2023

• test: add missing message

  mhuisi

  committed
  3b205d1

• test: adjust waiting logic for new activation logic

  mhuisi

  committed
  d3f06e4

• address unstable test?

  mhuisi

  committed
  dd1c480