commit 643e7946a1391eb6c5330f588faef7894b11db42
author Wim Jongman <wim.jongman@remainsoftware.com> Sun Jan 12 12:41:25 2020 +0100
committer Wim Jongman <wim.jongman@remainsoftware.com> Wed Jan 15 10:31:03 2020 -0500
tree ea2f0c30b74cb91a7611bc544c356b51e348e357
parent 0f8b5e41ffe3876da2ebb4d7c5f9a2bb8c06575d

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>