Merge branch 'dev' into favorites-gui

2023-02-03 21:58:34 -08:00
parent 143e5c6783 9a245c1acb
commit 2982f02328
39 changed files with 1583 additions and 929 deletions
--- a/rtdata/themes/TooWaBlue-GTK3-20_.css
+++ b/rtdata/themes/TooWaBlue-GTK3-20_.css
@@ -1281,6 +1281,11 @@ menuitem:hover > * {
    color: @text-hl-color;
 }

+menu menuitem > radio + * image:not(.dummy),
+#MyExpander menu menuitem > radio + * image:not(.dummy) {
+    margin-left: 1pt;
+}
+
 menu image:not(.dummy),
 #MyExpander menu image:not(.dummy) {
    min-height: 2em;