commit 41fc3142569fbfd4a40233da55a2b3f17cf6fa3e
author Andrey Loskutov <loskutov@gmx.de> Wed May 05 10:22:19 2021 +0200
committer Andrey Loskutov <loskutov@gmx.de> Wed May 05 07:54:41 2021 -0400
tree de4b134ad3567ada0e498751bb0f7a32f210449b
parent 44486007982366360ebadcee8557cac15dc91b04

Bug 573355 - Avoid double refresh after IDE crash

Allow org.eclipse.ui.ide.application to check if workspace crash was
detected, so it can skip (another one) workspace refresh in that case.

Change-Id: I8467f916eccb2f37877c1ff29bd01ecebda694b9
Signed-off-by: Andrey Loskutov <loskutov@gmx.de>
Reviewed-on: https://git.eclipse.org/r/c/platform/eclipse.platform.resources/+/180203
Tested-by: Platform Bot <platform-bot@eclipse.org>
Reviewed-by: Simeon Andreev <simeon.danailov.andreev@gmail.com>