Currently we have a tool filter in user settings, which can optionally be ignored (for non-restricted users only). It is frequently desirable to add/remove additional tools without completely ignoring toolfilter, and without editing user settings (which is permanent).
We should: