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.

Sign up for GitHub

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

Adjustments to VSCode <-> DevTools communication #197

Merged
merged 6 commits into from
Dec 11, 2024
Merged

Adjustments to VSCode <-> DevTools communication #197

Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
3700b50
Adjustments to VSCode <-> DevTools communication
phryneas Sep 11, 2024
277a5ad
use CI devtools build
phryneas Dec 6, 2024
c902746
feedback from code review
phryneas Dec 9, 2024
d4a65ee
second adjustment
phryneas Dec 9, 2024
7325a4d
adjust CI to GH runner changes
phryneas Dec 11, 2024
91967fe
Merge branch 'main' into pr/port-info
phryneas Dec 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
feedback from code review
  • Loading branch information
@phryneas
phryneas committed Dec 9, 2024
commit c902746991f5d7fa339342b41226f05cb71ef4fb
5 changes: 2 additions & 3 deletions src/devtools/server.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,10 +48,9 @@ export function startServer(port: number) {
if (serverState.port === port) {
// nothing to do
return;
} else {
// changing port, stop the old server
serverState.disposable.dispose();
}
// changing port, stop the old server
serverState.disposable.dispose();
}
serverState = state;
let wss: WebSocketServer | null = new WebSocketServer({ port });
Expand Down
Loading