From 139fe609e8360425b722b44167a8a0189ad79d53 Mon Sep 17 00:00:00 2001
From: "Davide P. Cervone" <dpvc@union.edu>
Date: Tue, 9 Jun 2026 07:47:27 -0400
Subject: [PATCH] Don't rerender the output during menu initialization.

---
 ts/ui/menu/Menu.ts | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/ts/ui/menu/Menu.ts b/ts/ui/menu/Menu.ts
index ebee11f7b..78b100f31 100644
--- a/ts/ui/menu/Menu.ts
+++ b/ts/ui/menu/Menu.ts
@@ -250,6 +250,8 @@ export class Menu {
    */
   protected document: MenuMathDocument;
 
+  protected initialized: boolean = false;
+
   /**
    * Instances of the various output jax that we can switch to
    */
@@ -566,6 +568,7 @@ export class Menu {
     this.mergeUserSettings();
     this.initMenu();
     this.applySettings();
+    this.initialized = true;
   }
 
   /**
@@ -1108,7 +1111,7 @@ export class Menu {
    */
   protected setOverflow(overflow: string) {
     this.document.outputJax.options.displayOverflow = overflow.toLowerCase();
-    if (!Menu.loading) {
+    if (!Menu.loading && this.initialized) {
       this.document.rerenderPromise();
     }
   }
@@ -1118,7 +1121,7 @@ export class Menu {
    */
   protected setInlineBreaks(breaks: boolean) {
     this.document.outputJax.options.linebreaks.inline = breaks;
-    if (!Menu.loading) {
+    if (!Menu.loading && this.initialized) {
       this.document.rerenderPromise();
     }
   }
@@ -1128,7 +1131,7 @@ export class Menu {
    */
   protected setScale(scale: string) {
     this.document.outputJax.options.scale = parseFloat(scale);
-    if (!Menu.loading) {
+    if (!Menu.loading && this.initialized) {
       this.document.rerenderPromise();
     }
   }