From b55784a985215d5766b9fc3ce6e9452b95637406 Mon Sep 17 00:00:00 2001 From: Miles Vella <673-vella@users.noreply.gitlab.cs.uni-duesseldorf.de> Date: Thu, 5 Sep 2024 14:53:53 +0200 Subject: [PATCH] try to fix hhu-stups/prob-issues#363 --- src/main/java/de/prob2/ui/beditor/BEditorView.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main/java/de/prob2/ui/beditor/BEditorView.java b/src/main/java/de/prob2/ui/beditor/BEditorView.java index d4516e93b..c43563e0f 100644 --- a/src/main/java/de/prob2/ui/beditor/BEditorView.java +++ b/src/main/java/de/prob2/ui/beditor/BEditorView.java @@ -539,6 +539,7 @@ private void setEditorText(String text, Path path) { beditor.moveTo(0); beditor.requestFollowCaret(); lastSavedText.set(beditor.getText()); + beditor.clearHistory(); // clear history again to forget setting of text, might fix hhu-stups/prob-issues#363 beditor.setEditable(true); LOGGER.debug("Setting editor text took {}", sw.stop()); } finally {