Fix #302 and clean up extraneous terminal margins (#303)

* font loading fix #302

* fix inconsistent paddings.  issue was that the first '[' feels indented (because of the fixed with font).  applying a negative 2px margin fixes it and allows us to remove the paddings on the other elements.
This commit is contained in:
Mike Sawka 2024-02-18 17:58:22 -08:00 committed by GitHub
parent fe3ffd1545
commit 07ad5f063e
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 6 additions and 13 deletions

View File

@ -84,11 +84,14 @@
} }
.meta.meta-line1 { .meta.meta-line1 {
margin-left: 2px;
color: rgba(@base-color, 0.6) !important; color: rgba(@base-color, 0.6) !important;
font-size: 11px; font-size: 11px;
} }
.meta.meta-line2 {
margin-left: -2px;
}
&.has-rtnstate .terminal-wrapper { &.has-rtnstate .terminal-wrapper {
padding-bottom: 0; padding-bottom: 0;
} }
@ -113,11 +116,6 @@
overflow-x: hidden; overflow-x: hidden;
} }
.terminal {
margin-right: 8px;
padding: 0.25rem;
}
&.cmd-done .terminal .xterm-cursor { &.cmd-done .terminal .xterm-cursor {
display: none; display: none;
} }

View File

@ -20,14 +20,9 @@ document.addEventListener("DOMContentLoaded", () => {
let reactElem = React.createElement(App, null, null); let reactElem = React.createElement(App, null, null);
let elem = document.getElementById("app"); let elem = document.getElementById("app");
let root = createRoot(elem); let root = createRoot(elem);
let isFontLoaded = document.fonts.check("12px 'JetBrains Mono'"); document.fonts.ready.then(() => {
if (isFontLoaded) {
root.render(reactElem); root.render(reactElem);
} else { });
document.fonts.ready.then(() => {
root.render(reactElem);
});
}
}); });
(window as any).mobx = mobx; (window as any).mobx = mobx;