From 07ad5f063ea0554d5a16e69c8511ac4dc01b7722 Mon Sep 17 00:00:00 2001 From: Mike Sawka Date: Sun, 18 Feb 2024 17:58:22 -0800 Subject: [PATCH] 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. --- src/app/line/lines.less | 10 ++++------ src/index.ts | 9 ++------- 2 files changed, 6 insertions(+), 13 deletions(-) diff --git a/src/app/line/lines.less b/src/app/line/lines.less index 520eee0a..19c5bc62 100644 --- a/src/app/line/lines.less +++ b/src/app/line/lines.less @@ -84,11 +84,14 @@ } .meta.meta-line1 { - margin-left: 2px; color: rgba(@base-color, 0.6) !important; font-size: 11px; } + .meta.meta-line2 { + margin-left: -2px; + } + &.has-rtnstate .terminal-wrapper { padding-bottom: 0; } @@ -113,11 +116,6 @@ overflow-x: hidden; } - .terminal { - margin-right: 8px; - padding: 0.25rem; - } - &.cmd-done .terminal .xterm-cursor { display: none; } diff --git a/src/index.ts b/src/index.ts index 7b415a4b..87ebfcf2 100644 --- a/src/index.ts +++ b/src/index.ts @@ -20,14 +20,9 @@ document.addEventListener("DOMContentLoaded", () => { let reactElem = React.createElement(App, null, null); let elem = document.getElementById("app"); let root = createRoot(elem); - let isFontLoaded = document.fonts.check("12px 'JetBrains Mono'"); - if (isFontLoaded) { + document.fonts.ready.then(() => { root.render(reactElem); - } else { - document.fonts.ready.then(() => { - root.render(reactElem); - }); - } + }); }); (window as any).mobx = mobx;