Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Problem with PowerShell ExecutionPolicy #216

Closed
lovettchris opened this issue Jul 11, 2022 · 0 comments · Fixed by #217
Closed

Problem with PowerShell ExecutionPolicy #216

lovettchris opened this issue Jul 11, 2022 · 0 comments · Fixed by #217

Comments

@lovettchris
Copy link
Contributor

lovettchris commented Jul 11, 2022

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/VSCode.20.22Waiting.20for.20lean.20server.20to.20start.2E.2E.2E.22

Students may not know how to run Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope CurrentUser needed in order for elan-init.ps1 to work.

We could run it for them before running elan-init.ps1 then set it back to whatever level it was before. We can also set a safer level of Set-ExecutionPolicy -ExecutionPolicy RemoteSigned -Scope CurrentUser which still works because elan-init.ps1 is run locally, not remotely.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant