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 description of VSCode extensions #226

Merged
merged 2 commits into from
Oct 4, 2023

Conversation

gares
Copy link
Member

@gares gares commented Oct 3, 2023

The info was outdated. This is a minimal fix.

@gares gares requested a review from Zimmi48 October 3, 2023 15:42
@herbelin
Copy link
Member

herbelin commented Oct 3, 2023

Looks good to me (and this is was somehow awaited information to take decisions on #218)

@herbelin
Copy link
Member

herbelin commented Oct 3, 2023

BTW, does this mean that the VsCoq 1 vs VsCoq 2 difference of terminology disappears and that VsCoq 1 is just considered an old non-lsp variant of VsCoq?

@gares
Copy link
Member Author

gares commented Oct 3, 2023

I'll leave to the home pages of the projects to detail these things.
If we put too much info here it is going to be outdated too soon imo.

@herbelin
Copy link
Member

herbelin commented Oct 3, 2023

I'll leave to the home pages of the projects to detail these things.

OK. It that I was afraid that the text "Both extensions are based on LSP" led to confusion if VsCoq 1 is still an option.

Copy link
Member

@Zimmi48 Zimmi48 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a much-needed fix, and since we didn't manage to converge on a description that would say more, I agree that it is reasonable to defer additional explanations to the projects' webpage.

Just a minor suggested change to clarify the situation for users who were already aware of the existence of VsCoq before.

pages/user-interfaces.html Outdated Show resolved Hide resolved
@herbelin
Copy link
Member

herbelin commented Oct 4, 2023

we didn't manage to converge on a description that would say more

If you are referring to #218, I should talk with Emilio but it may converge. This PR (#226) is however needed.

Co-authored-by: Théo Zimmermann <[email protected]>
@gares
Copy link
Member Author

gares commented Oct 4, 2023

Done, I let you merge @Zimmi48 / @herbelin !

@Zimmi48 Zimmi48 merged commit 98a00d1 into master Oct 4, 2023
4 checks passed
@Zimmi48 Zimmi48 deleted the update-vscode-ext-description branch October 4, 2023 10:41
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 this pull request may close these issues.

3 participants