tree ea2f0c30b74cb91a7611bc544c356b51e348e357
parent 0f8b5e41ffe3876da2ebb4d7c5f9a2bb8c06575d
author Wim Jongman <wim.jongman@remainsoftware.com> 1578829285 +0100
committer Wim Jongman <wim.jongman@remainsoftware.com> 1579102263 -0500

Bug 540662 - [Tips] Preference to unsubscribe from a Tip Provider

This change adds supports for disabling and enabling providers. The
preference can be specified via product customization, with the
following line:

org.eclipse.tips.ide/disabled_providers=<comma sep list of provider ids>

This patch provides additional coding to prevent initializing of the
preferences on every call.

Change-Id: I636c537ba4fbd51cee7915c9e452e2b03b5caa65
Signed-off-by: Wim Jongman <wim.jongman@remainsoftware.com>