mirror of
https://github.com/arduino/arduino-ide.git
synced 2025-11-16 13:49:28 +00:00
Enhance MonitorManager APIs
This commit is contained in:
committed by
Alberto Iannaccone
parent
2c95e7f033
commit
480492a7c8
@@ -1,12 +0,0 @@
|
||||
import { JsonRpcServer } from "@theia/core";
|
||||
|
||||
export const MonitorManagerProxyPath = '/services/monitor-manager-proxy';
|
||||
export const MonitorManagerProxy = Symbol('MonitorManagerProxy');
|
||||
export interface MonitorManagerProxy extends JsonRpcServer<MonitorManagerProxyClient> {
|
||||
|
||||
}
|
||||
|
||||
export const MonitorManagerProxyClient = Symbol('MonitorManagerProxyClient');
|
||||
export interface MonitorManagerProxyClient {
|
||||
|
||||
}
|
||||
Reference in New Issue
Block a user