Work-around for window position not always changing on first update() call.

2022-11-21 22:21:29 +01:00 · 2022-11-21 22:21:29 +01:00 · 9ba2ae0749
parent 2731eeaa45
commit 9ba2ae0749
1 changed files with 7 additions and 5 deletions
--- a/src/ui/prompt.js
+++ b/src/ui/prompt.js
@ -136,11 +136,13 @@
    }
    let win = await browser.windows.getCurrent();
    let delta = document.documentElement.offsetHeight - window.innerHeight;
+    for (let attempts = 2; attempts-- > 0;) {
      await browser.windows.update(win.id, {
        height: win.height + delta,
        top: win.top - Math.round(delta / 2),
        focused: false
      });
+    }
    await browser.windows.update(win.id, {focused: true});
  }
  if (document.readyState === "complete") {