I20210601-1800
Added a configuration whether history for derived files is kept. Off (no history for derived files) by default. Change-Id: I9e4e7fdeb1cbb690c400ce03d231feff82b4ca08 Signed-off-by: Joerg Kubitz <jkubitz-eclipse@gmx.de> Reviewed-on: https://git.eclipse.org/r/c/platform/eclipse.platform.ui/+/180357 Tested-by: Lars Vogel <Lars.Vogel@vogella.com> Reviewed-by: Lars Vogel <Lars.Vogel@vogella.com>