June 9, 2018
6:21 p.m.
Le 09/06/2018 à 18:24, Cyril Ferlicot D. a écrit :
It was here but in a different hook. It was in setDefaultParameters as you can see here:
https://github.com/pharo-project/pharo/pull/1479/files#diff-f9fc80b09f7cbc9c...
I see.
Next, why docking bar should have the same width as menu?
It was the previous behavior. What I changed is that now #themeChanged reset the border width to take the one of the current theme when before it was ignored.
The question is do we want docking bar to have border?
I'll probably propose a new method in the theme #dockingBarBorderWidth and we can return 0 by default for it.
That way, it will be easy to change it with specific theme. Thanks Hilaire -- Dr. Geo http://drgeo.eu