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

update README to clearly label as for Lean 3 #338

Closed
kim-em opened this issue Sep 7, 2023 · 1 comment
Closed

update README to clearly label as for Lean 3 #338

kim-em opened this issue Sep 7, 2023 · 1 comment

Comments

@kim-em
Copy link
Contributor

kim-em commented Sep 7, 2023

and add a prominent notice at the top of the README that this is for an old version of the language, and that users should use the lean4 extension instead.

@kim-em
Copy link
Contributor Author

kim-em commented Sep 7, 2023

@mhuisi

mhuisi added a commit to mhuisi/vscode-lean that referenced this issue Sep 8, 2023
@gebner gebner closed this as completed in 1589ca3 Sep 17, 2023
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

No branches or pull requests

1 participant