Re: How to change docker arrow icon size?

2023-01-09 Thread Thomas Passin
The plugin is *nav_qt.py*. On Tuesday, January 10, 2023 at 12:11:46 AM UTC-5 Thomas Passin wrote: > The height would probably be set in the CSS rules in the theme's qt > stylesheet. I'm not sure just now which selector would cover it. The > arrows must be icons somewhere, but you'd probably h

Re: How to change docker arrow icon size?

2023-01-09 Thread Thomas Passin
The height would probably be set in the CSS rules in the theme's qt stylesheet. I'm not sure just now which selector would cover it. The arrows must be icons somewhere, but you'd probably have to look in the plugin's code to find them. On Monday, January 9, 2023 at 9:02:31 PM UTC-5 wangz...@g

How to change docker arrow icon size?

2023-01-09 Thread zhaohe wang
Help! Is there a way to change docker hight or arrow size. It seems the arrow is bigger. [image: iShot_2023-01-10_10.01.02.png] -- You received this message because you are subscribed to the Google Groups "leo-editor" group. To unsubscribe from this group and stop receiving emails from it, sen

Re: Abbreviations For Greek Letters

2023-01-09 Thread Thomas Passin
because;;=∵ That's one I've never heard of before! An inverted "therefore". On Monday, January 9, 2023 at 5:52:18 PM UTC-5 Edward K. Ream wrote: > On Mon, Jan 9, 2023 at 4:48 PM Rob wrote: > >> Perhaps also useful: >> >> degree;;=° >> half;;=½ >> quarter;;=¼ >> 3fourths;;=¾ >> divide;;=÷ >> bull

Re: Abbreviations For Greek Letters

2023-01-09 Thread Edward K. Ream
On Mon, Jan 9, 2023 at 4:48 PM Rob wrote: > Perhaps also useful: > > degree;;=° > half;;=½ > quarter;;=¼ > 3fourths;;=¾ > divide;;=÷ > bullet;;=• > infinity;;=∞ > # Ellipsis > ...;;=… > ergo;;=∴ > because;;=∵ > > # Currency > cent;;=¢ > euro;;=€ > pound;;=£ > yen;;=¥ > Thanks. Rev 45b20a7 in dev

Re: Abbreviations For Greek Letters

2023-01-09 Thread Edward K. Ream
On Mon, Jan 9, 2023 at 3:16 PM Thomas Passin wrote: > Maybe in the section in LeoDocs that mentions abbreviations? Rev 353404b in devel adds the disabled version of these abbreviations to `@data abbreviations` in leoSettings.leo. The node has this comment: "Typically you would define @data glo

Re: Abbreviations For Greek Letters

2023-01-09 Thread Rob
Perhaps also useful: degree;;=° half;;=½ quarter;;=¼ 3fourths;;=¾ divide;;=÷ bullet;;=• infinity;;=∞ # Ellipsis ...;;=… ergo;;=∴ because;;=∵ # Currency cent;;=¢ euro;;=€ pound;;=£ yen;;=¥ On Monday, January 9, 2023 at 5:34:32 PM UTC-5 Edward K. Ream wrote: > On Mon, Jan 9, 2023 at 1:32 PM Rob

Re: Abbreviations For Greek Letters

2023-01-09 Thread Edward K. Ream
On Mon, Jan 9, 2023 at 1:32 PM Rob wrote: > The abbreviation definitions must be copied into a settings node, best >> placed in *myLeoSettings.leo*, and the node's headline must start with *@data >> global-abbreviations* to make them available in all outlines. My node >> has the headline >> *@d

Re: Leo's new website is live. Leo 6.7.2 coming soon

2023-01-09 Thread Edward K. Ream
On Mon, Jan 9, 2023 at 3:11 PM Thomas Passin wrote: > One glitch - Links from the google search box point to the old site, not > the new one. > Good catch! I've added this bug to the checklist for #3019 , so there is no need for a separate is

Re: Abbreviations For Greek Letters

2023-01-09 Thread Thomas Passin
Maybe in the section in LeoDocs that mentions abbreviations? It's very short, and these shortcuts could serve as examples, too. @Edward suggested disabled in LeoSettings.leo. That would be all right too, but how many of us troll through there looking for interesting things? I expect my own l

Re: Leo's new website is live. Leo 6.7.2 coming soon

2023-01-09 Thread Thomas Passin
Great! One glitch - Links from the google search box point to the old site, not the new one. On Monday, January 9, 2023 at 1:45:53 PM UTC-5 Edward K. Ream wrote: > GitHub pages now hosts Leo's new website at: > https://leo-editor.github.io/leo-editor/ > > Please test these new pages and report

Re: Abbreviations For Greek Letters

2023-01-09 Thread Rob
Thanks for the list! I do much the same thing and have an even longer list; not just Greek letters. Is there a better place to add to the list than here? Rob... On Sunday, January 8, 2023 at 2:19:32 PM UTC-5 tbp1...@gmail.com wrote: > Sometimes I want to insert a Greek letter into text, often

Leo's new website is live. Leo 6.7.2 coming soon

2023-01-09 Thread Edward K. Ream
GitHub pages now hosts Leo's new website at: https://leo-editor.github.io/leo-editor/ Please test these new pages and report any problems! There will be a period of transition, as described in #3019 . To avoid confusion, the new home page ha