diff --git a/collects/mred/private/kernel.ss b/collects/mred/private/kernel.ss index 326639d2..9e87c57b 100644 --- a/collects/mred/private/kernel.ss +++ b/collects/mred/private/kernel.ss @@ -203,6 +203,7 @@ num-scroll-lines scroll-line-location get-snip-location + in-edit-sequence? refresh-delayed? end-edit-sequence begin-edit-sequence