tree de4b134ad3567ada0e498751bb0f7a32f210449b
parent 44486007982366360ebadcee8557cac15dc91b04
author Andrey Loskutov <loskutov@gmx.de> 1620202939 +0200
committer Andrey Loskutov <loskutov@gmx.de> 1620215681 -0400

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>