Merge branch 'v8.5'

1 files changed, 10 insertions, 2 deletions

diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 1f3990708a..5d21efd956 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -186,11 +186,19 @@ object(self)
 
   method undo () =
     Minilib.log "UNDO";
-    self#with_lock_undo self#perform_undo ();
+    self#with_lock_undo begin fun () ->
+      buffer#begin_user_action ();
+      self#perform_undo ();
+      buffer#end_user_action ()
+    end ()
 
   method redo () =
     Minilib.log "REDO";
-    self#with_lock_undo self#perform_redo ();
+    self#with_lock_undo begin fun () ->
+      buffer#begin_user_action ();
+      self#perform_redo ();
+      buffer#end_user_action ()
+    end ()
 
   method process_begin_user_action () =
     (* Push a new level of event on history stack *)