MARGIN_IN_PIXELS 5631 src/window.c         return (unit == MARGIN_IN_PIXELS)
MARGIN_IN_PIXELS 6022 src/window.c     this_scroll_margin = window_scroll_margin (w, MARGIN_IN_PIXELS);
MARGIN_IN_PIXELS 18498 src/xdisp.c      this_scroll_margin = window_scroll_margin (w, MARGIN_IN_PIXELS);
MARGIN_IN_PIXELS 18997 src/xdisp.c          this_scroll_margin = window_scroll_margin (w, MARGIN_IN_PIXELS);
MARGIN_IN_PIXELS 20777 src/xdisp.c          int top_scroll_margin = window_scroll_margin (w, MARGIN_IN_PIXELS);
MARGIN_IN_PIXELS 22129 src/xdisp.c        int top_scroll_margin = window_scroll_margin (w, MARGIN_IN_PIXELS);