1
0
mirror of https://github.com/emilk/egui.git synced 2026-06-27 07:03:14 -04:00

Fix edge-case in duplicate ID warning

This commit is contained in:
Emil Ernerfeldt
2020-12-16 20:28:43 +01:00
parent f1b4353039
commit 471314bb44

View File

@@ -342,7 +342,7 @@ impl Context {
/// Call this for `Id`:s that need interaction or persistence.
pub(crate) fn register_interaction_id(self: &Arc<Self>, id: Id, new_pos: Pos2) {
if let Some(prev_pos) = self.memory().used_ids.insert(id, new_pos) {
if prev_pos == new_pos {
if prev_pos.distance(new_pos) < 0.1 {
// Likely same Widget being interacted with twice, which is fine.
return;
}