You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I have the weirdest problem with this error. I get it from a bare bones "cmd.exe" on my machine and in my github ci on "windows-latest". But if I run the test in VS code using my Extension Tests - lean3 launch configuration it runs fine, and if I run it from a Visual Studio Developer Command prompt it runs fine (but I should totally not need a vs developer prompt to run these tests). The repro is this:
I have the weirdest problem with this error. I get it from a bare bones "cmd.exe" on my machine and in my github ci on "windows-latest". But if I run the test in VS code using my Extension Tests - lean3 launch configuration it runs fine, and if I run it from a Visual Studio Developer Command prompt it runs fine (but I should totally not need a vs developer prompt to run these tests). The repro is this:
The test begins, it downloads a test version of vscode, vscode launches, but then the mocha.run blows up with this error:
My tests are "ui: tdd" tests which is specified in my index.ts so I'm not sure why it's even looking for
describe
...But here's the most ridiculous part. If I run this
then type this:
Then the tests run fine, no problem with mocha. Even weirder, if I do this:
Then type:
It seems to have something to do with the casing of the "D:" drive letter? If I run "pushd D:\git\leanprover\vscode-lean4" then the test fails...
The text was updated successfully, but these errors were encountered: