diff options
| -rw-r--r-- | doc/emacs/frames.texi | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/doc/emacs/frames.texi b/doc/emacs/frames.texi index 06e93438ed2..bd836b2db65 100644 --- a/doc/emacs/frames.texi +++ b/doc/emacs/frames.texi | |||
| @@ -98,7 +98,7 @@ invoked by clicking with the left mouse button, @kbd{mouse-1}, in the | |||
| 98 | text area of a window. This moves point to the position where you | 98 | text area of a window. This moves point to the position where you |
| 99 | clicked. If that window was not the selected window, it becomes the | 99 | clicked. If that window was not the selected window, it becomes the |
| 100 | selected window. You can also activate a region by double-clicking | 100 | selected window. You can also activate a region by double-clicking |
| 101 | mouse-1 (@pxref{Word and Line Mouse}). | 101 | @kbd{mouse-1} (@pxref{Word and Line Mouse}). |
| 102 | 102 | ||
| 103 | @vindex x-mouse-click-focus-ignore-position | 103 | @vindex x-mouse-click-focus-ignore-position |
| 104 | Normally, if the frame you clicked in was not the selected frame, it | 104 | Normally, if the frame you clicked in was not the selected frame, it |
| @@ -998,7 +998,9 @@ when the entire buffer is visible. | |||
| 998 | 998 | ||
| 999 | @cindex scroll-bar face | 999 | @cindex scroll-bar face |
| 1000 | The visual appearance of the scroll bars is controlled by the | 1000 | The visual appearance of the scroll bars is controlled by the |
| 1001 | @code{scroll-bar} face. | 1001 | @code{scroll-bar} face. (Some toolkits, such as GTK and MS-Windows, |
| 1002 | ignore this face; the scroll-bar appearance there can only be | ||
| 1003 | customized system-wide, for GTK @pxref{GTK resources}). | ||
| 1002 | 1004 | ||
| 1003 | @cindex vertical border | 1005 | @cindex vertical border |
| 1004 | On graphical frames, vertical scroll bars implicitly serve to separate | 1006 | On graphical frames, vertical scroll bars implicitly serve to separate |
| @@ -1073,7 +1075,7 @@ customize the options @code{window-divider-default-bottom-width} and | |||
| 1073 | @code{window-divider-default-right-width}. | 1075 | @code{window-divider-default-right-width}. |
| 1074 | 1076 | ||
| 1075 | When vertical scroll bars are disabled, dividers can be also useful to | 1077 | When vertical scroll bars are disabled, dividers can be also useful to |
| 1076 | make the first pixel column of a window visible which would be otherwise | 1078 | make the first pixel column of a window visible, which would be otherwise |
| 1077 | covered by the vertical border used to separate side-by-side windows | 1079 | covered by the vertical border used to separate side-by-side windows |
| 1078 | (@pxref{Scroll Bars}). | 1080 | (@pxref{Scroll Bars}). |
| 1079 | 1081 | ||