2019-08-07 08:26:53 +00:00
|
|
|
import { WebSocketMessage } from './websocket-message';
|
2018-05-31 10:02:53 +00:00
|
|
|
|
2019-08-08 12:44:40 +00:00
|
|
|
export interface IDEMessage extends WebSocketMessage {
|
2018-04-20 07:21:20 +00:00
|
|
|
filename: string;
|
|
|
|
content?: string;
|
2019-08-07 08:26:53 +00:00
|
|
|
files?: string[];
|
2020-05-26 13:34:54 +00:00
|
|
|
reload?: boolean;
|
2018-04-20 07:21:20 +00:00
|
|
|
}
|