tree 1ccc6b0facac237807c28db4c5d0632db34d410e
parent 61d7571217e47f583bc5b3e1aeaa775322cbd7e6
author Joerg Kubitz <jkubitz-eclipse@gmx.de> 1620391675 +0200
committer Lars Vogel <Lars.Vogel@vogella.com> 1621790652 -0400

Bug 573421 - Avoid local history for derived files (UI)

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>