|
@@ -119,10 +119,10 @@ class TerminalWidget extends Widget {
|
|
|
// Set the default title.
|
|
|
this.title.text = 'Terminal ' + TerminalWidget.nterms;
|
|
|
|
|
|
- this._dummyTerm = createDummyTerm();
|
|
|
-
|
|
|
Terminal.brokenBold = true;
|
|
|
|
|
|
+ this._dummyTerm = createDummyTerm();
|
|
|
+
|
|
|
this._ws.onopen = (event: MessageEvent) => {
|
|
|
this._createTerm(options);
|
|
|
};
|