Re: [Notion-devel] [Notion-general] Notion 4

[Dima K. <no...@di...>]

Arnout Engelen <ar...@bz...> writes:

> On Sun, Oct 6, 2019 at 6:05 AM Dima Kogan <no...@di...> wrote:
>> I still see some look-related issues that aren't fixed with any based_on invocation I
>> tried:
>>
>> 1. In my look the empty-pane color used to be black, but now it's gray.
>>    Empty panes come up when I create a new workspace with
>>    ioncore.create_ws(_). This is also the filler color used to cover
>>    empty space if a window doesn't completely fill a tab. Do you know
>>    what style thing controls this?
>>
>> 2. I think the margin between the top of the tab bar and the top of the
>>    screen has increased by a few pixels. Do you know what controls this?
>>
>> 3. Menus that pop up with mod_menu are now using a different font. For
>>    instance, the main menu: mod_menu.menu(_, _sub, 'mainmenu',
>>    {big=true}). Do you know where this font is set? It also looks weird
>>    on my machine, and I suspect my box doesn't actually HAVE this font.
>>    So there could also be a packaging issue I need to look at. Any way
>>    to tell what font it's trying to use?
>
> Could you share the custom look you're using here? Are you using an
> external compositor?

Sure. No external anything; everything is vanilla. The look is attached.
It's a very-lightly hacked look_ios.lua. I don't remember exactly what I
was going for when I settled on this; it was a very long time ago.