commit 6100ecd8a9da560a70f7f5eed283dc1002551715
author Simeon Andreev <simeon.danailov.andreev@gmail.com> Tue Nov 06 13:15:38 2018 +0100
committer Simeon Andreev <simeon.danailov.andreev@gmail.com> Tue Nov 06 15:00:20 2018 +0100
tree f7a0616012158a161c06404de44ef45ac207c81e
parent 41e56139f31670455d0c982d3baceb314c0a5cc5

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

This change adds a preference which can disable specific tip providers.
The preference then lists tip provider ids separated by commas. The
preference can be specified via product customization, with the
following line:

org.eclipse.tips.ide/disabled_providers=org.eclipse.tips.ide.internal.provider.TipsTipProvider,org.eclipse.tips.ide.internal.provider.TwitterTipProvider

Change-Id: I133e4ef90b6272254d10ef0c76149d7c04385d8c
Signed-off-by: Simeon Andreev <Simeon.Andreev@NashTech.com>