Merge branch 'dev' into release/v0.8.2

This commit is contained in:
cschen 2024-10-26 19:48:38 +02:00 committed by GitHub
commit 551044ef20
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 4 deletions

View file

@ -30,7 +30,6 @@ jobs:
toolchain:
- stable
- beta
- nightly
steps:
- uses: arduino/setup-protoc@v3
with:
@ -49,7 +48,6 @@ jobs:
toolchain:
- stable
- beta
- nightly
steps:
- uses: arduino/setup-protoc@v3
with:

View file

@ -324,8 +324,9 @@ function Workspace:fetch_users(path) end
function Workspace:fetch_buffer_users(path) end
---@class (exact) WorkspaceEvent
---@field type string
---@field value string
---@field type string can be "UserJoin", "UserLeave" or "FileTreeUpdated"
---@field name? string present for "UserJoin" and "UserLeave"
---@field path? string present for "FileTreeUpdated"
---@return MaybeWorkspaceEventPromise
---@async