Merge branch 'master' into gui_search

2022-08-03 00:44:17 -07:00
parent b0a55c9b18
commit 51982dde62
79 changed files with 6320 additions and 6336 deletions
--- a/theseus_gui/src/layout/StatusBar.svelte
+++ b/theseus_gui/src/layout/StatusBar.svelte
@@ -75,6 +75,7 @@
        color: var(--color-text-lightest);
      }
    }
+  }

    .statuses {
      margin-left: auto;