Set height to 0 if domNode is null.

This commit is contained in:
Henning Dieterichs 2021-11-26 10:56:41 +01:00
parent 75d09de705
commit ab8b0b914a
No known key found for this signature in database
GPG key ID: 771381EFFDB9EC06

View file

@ -1492,13 +1492,13 @@ export class CodeEditorWidget extends Disposable implements editorBrowser.ICodeE
Configuration.applyFontInfoSlow(target, this._configuration.options.get(EditorOption.fontInfo)); Configuration.applyFontInfoSlow(target, this._configuration.options.get(EditorOption.fontInfo));
} }
public setBanner(domNode: HTMLElement | null, height: number): void { public setBanner(domNode: HTMLElement | null, domNodeHeight: number): void {
if (this._bannerDomNode && this._domElement.contains(this._bannerDomNode)) { if (this._bannerDomNode && this._domElement.contains(this._bannerDomNode)) {
this._domElement.removeChild(this._bannerDomNode); this._domElement.removeChild(this._bannerDomNode);
} }
this._bannerDomNode = domNode; this._bannerDomNode = domNode;
this._configuration.reserveHeight(height); this._configuration.reserveHeight(domNode ? domNodeHeight : 0);
if (this._bannerDomNode) { if (this._bannerDomNode) {
this._domElement.prepend(this._bannerDomNode); this._domElement.prepend(this._bannerDomNode);