mirror of
https://github.com/arduino/arduino-ide.git
synced 2025-07-30 14:46:34 +00:00
Fixed WebSocketChange event signature
This commit is contained in:
parent
480492a7c8
commit
c5695d3a76
@ -1,6 +1,6 @@
|
|||||||
import { Emitter } from "@theia/core";
|
import { Emitter } from "@theia/core";
|
||||||
import { injectable } from "@theia/core/shared/inversify";
|
import { injectable } from "@theia/core/shared/inversify";
|
||||||
import { MonitorManagerProxyClient } from "../common/monitor-manager-proxy";
|
import { MonitorManagerProxyClient } from "../common/protocol/monitor-service";
|
||||||
|
|
||||||
@injectable()
|
@injectable()
|
||||||
export class MonitorManagerProxyClientImpl implements MonitorManagerProxyClient {
|
export class MonitorManagerProxyClientImpl implements MonitorManagerProxyClient {
|
||||||
|
@ -10,8 +10,8 @@ export interface MonitorManagerProxy extends JsonRpcServer<MonitorManagerProxyCl
|
|||||||
|
|
||||||
export const MonitorManagerProxyClient = Symbol('MonitorManagerProxyClient');
|
export const MonitorManagerProxyClient = Symbol('MonitorManagerProxyClient');
|
||||||
export interface MonitorManagerProxyClient {
|
export interface MonitorManagerProxyClient {
|
||||||
onWebSocketChanged: Event<string>;
|
onWebSocketChanged: Event<number>;
|
||||||
notifyWebSocketChanged(message: string): void;
|
notifyWebSocketChanged(message: number): void;
|
||||||
}
|
}
|
||||||
|
|
||||||
export interface MonitorSetting {
|
export interface MonitorSetting {
|
||||||
|
Loading…
x
Reference in New Issue
Block a user