-
Halla Rempt authored
Even though the toolbox's closable feature was set to off, it was possible to lose the toolbox. Not having the toolbox in the menu meant that it is impossible to re-add it without resetting the entire workspace. This has happened to dozens of people now, so it's clear that it's better to make the toolbox and ordinary toggable docker. Besides, advanced users might actually only activate tools with the shortcuts, so for them, the toolbox is clutter.
29bbb05c