On sam. 9 juin 2018 at 09:48, Hilaire <[email protected]> wrote: > Why ? > > DockingBarMorph>>defaultBorderWidth > ^ self theme menuBorderWidth >
I found the PR I did. This code was already here but in another method. The difference is that now #themeChanged take the borderWidth into account. Before it ignored it. So it's probably that before there was a bug where the docking bar did not matched the theme for the border and it was corrected. Now, without the bug, you found that the theme was not as good as you wanted and we need to update the theme. > > Le 09/06/2018 à 09:27, Hilaire a écrit : > > I am not there yet, hope to have time. Now I just browse changes from > > github, can see several changed related to use of theme borderwidth > > -- > Dr. Geo > http://drgeo.eu > > > > -- Cyril Ferlicot https://ferlicot.fr
