tweaks: always directly do a refresh when the margin changes
The previous code only directly refreshed the screen when the margin changed due to toggling line numbering on. When the margin changed due to toggling it off, it would indirectly refresh via do_toggle().
Showing
+9 -15
Please register or sign in to comment