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-f9fc80b09f7cbc9cb0b3f63560dabd23L613
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
