diff options
| -rw-r--r-- | ide/.coqiderc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/.coqiderc b/ide/.coqiderc index 68d0a56c44..43883c5ff2 100644 --- a/ide/.coqiderc +++ b/ide/.coqiderc @@ -1,6 +1,6 @@ binding "text" { bind "<ctrl>k" { "set-anchor" () - "move-cursor" (paragraphs,1,0) + "move-cursor" (display-lines,1,0) "cut-clipboard" () } bind "<ctrl>x" { } |