fix region list not updating upon deletion

DecwLK · Mar 10, 2024 · 080831a · 080831a
1 parent 8c16126
commit 080831a
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/main/java/org/gecko/actions/DeleteRegionViewModelElementAction.java b/src/main/java/org/gecko/actions/DeleteRegionViewModelElementAction.java
@@ -26,6 +26,7 @@ public class DeleteRegionViewModelElementAction extends AbstractPositionableView
     boolean run() throws GeckoException {
         automaton.removeRegion(regionViewModel.getTarget());
         geckoViewModel.deleteViewModelElement(regionViewModel);
+        geckoViewModel.getCurrentEditor().updateRegions();
         return true;
     }