Add zed://extension/{id} links (#34492)

Release Notes:

- Add zed://extension/{id} links to open the extensions UI with a
specific extension
This commit is contained in:
Conrad Irwin 2025-07-15 13:42:25 -06:00 committed by GitHub
parent ec52e9281a
commit 3751737621
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
9 changed files with 72 additions and 10 deletions

View file

@ -76,6 +76,9 @@ pub struct Extensions {
/// Filters the extensions page down to extensions that are in the specified category.
#[serde(default)]
pub category_filter: Option<ExtensionCategoryFilter>,
/// Focuses just the extension with the specified ID.
#[serde(default)]
pub id: Option<String>,
}
/// Decreases the font size in the editor buffer.