-
Kai Koehne authored
Save/restore the current settings of a navigation widget per position, every time something changes in the navigation bar setup. Previously, only settings on exit were stored / restored on startup, which means that e.g. when you switch from the Outline to the Project Explorer and back, the settings of the Outline were lost. Reviewed-by: con
802b21c0