Résoud #2218 : Supprimer aussi des préférences l'option 'masquer les outils'...

Résoud #2218 : Supprimer aussi des préférences l'option 'masquer les outils' supprimée par r18208 car contre-intuitive d'un point de vue ergonomique.