repl input: tune line height

This commit is contained in:
isidor 2016-08-05 15:59:12 +02:00
parent b4937be487
commit 07f2b9dab9

View file

@ -183,7 +183,7 @@ export class Repl extends Panel {
this.tree.refresh().done(undefined, errors.onUnexpectedError);
}
this.replInput.layout({ width: dimension.width - 20, height: 22 });
this.replInput.layout({ width: dimension.width - 20, height: 21 });
}
public focus(): void {
@ -224,9 +224,9 @@ export class Repl extends Panel {
horizontal: 'hidden',
vertical: 'hidden'
},
lineDecorationsWidth:0,
lineDecorationsWidth: 0,
scrollBeyondLastLine: false,
lineHeight: 20,
lineHeight: 21,
theme: this.themeService.getTheme()
};