try to fix hhu-stups/prob-issues#363

hhu-stups · Sep 5, 2024 · b55784a · b55784a
1 parent 3f933d0
commit b55784a
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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 {