key icon indicating copy to clipboard operation
key copied to clipboard

Published 20 hours ago • verified publisher icon KeYProject

Revert "Fix CurrentGoalView highlights not being removed"

Open mattulbrich opened this issue 1 year ago • 4 comments

Related Issue

This pull request addresses #3378.

Intended Change

This reverts commit 4759370f719ed506746e7a2a13832eac48cfc6c1.

As discussed during a developers meeting, the highlighting is quite important during drag'n'drop.

It reenables the highlighter when drag-n-dropping terms. Moreover, it repairs heatmap toggling.

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)

Ensuring quality

  • I have tested the feature as follows: Tried it in the gui

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

mattulbrich avatar Jan 30 '24 10:01 mattulbrich