search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
158 stars 48 forks source link

Overview missing in VSCode Marketplace #493

Closed bryangingechen closed 2 months ago

bryangingechen commented 3 months ago

Description

The lean4 extension page on the VS Code marketplace says: No overview has been entered by publisher.

Here's what it looks like when searching from within VS Code:

Screenshot 2024-07-02 at 18 38 12

I'm guesssing the main README file from this repo would be suitable as an overview for the extension, but the file isn't being included in the .vsix file that is being published.

Expected behavior: The README file from this repo appears.

Actual behavior: See above.

Impact

People might be suspicious of an extension with a blank overview.

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

mhuisi commented 2 months ago

We have a new README that refers to the setup guide and the manual now and it is displayed in the VS Code marketplace. (#501, #502, #503)