edit_command_buffer: repaint

Thanks @amosbird on gitter.
2024-11-25 18:03:37 +08:00 · 2018-10-25 17:34:01 +02:00 · 2018-10-25 17:34:01 +02:00 · c78e6a3ccf
commit c78e6a3ccf
parent fb0c1460a9
1 changed files with 3 additions and 0 deletions
--- a/share/functions/edit_command_buffer.fish
+++ b/share/functions/edit_command_buffer.fish
@ -45,4 +45,7 @@ function edit_command_buffer --description 'Edit the command buffer in an extern
        echo (_ "or the file was empty")
    end
    command rm $f
+    # We've probably opened something that messed with the screen.
+    # A repaint seems in order.
+    commandline -f repaint
 end