Update two user option names in the Widget manual

* doc/misc/widget.texi (Basic Types): The user options
widget-glyph-directory and widget-glyph-enable were renamed long ago
to widget-image-directory and widget-image-enable, but the manual
kept calling them by their old names.  Update the names.

diff --git a/doc/misc/widget.texi b/doc/misc/widget.texi
index 6f0b63e5bf4a0f800633e3cefba2258357ff215a..64cbf8d950ab64d8243da1b45f0debdd4fd08152 100644 (file)
--- a/doc/misc/widget.texi
+++ b/doc/misc/widget.texi
@@ -692,14 +692,14 @@ arguments, which will be used when creating the @code{radio-button} or
 
 @end table
 
-@deffn {User Option} widget-glyph-directory
-Directory where glyphs are found.
+@deffn {User Option} widget-image-directory
+Directory where Widget should look for images.
 Widget will look here for a file with the same name as specified for the
 image, with either a @file{.xpm} (if supported) or @file{.xbm} extension.
 @end deffn
 
-@deffn{User Option} widget-glyph-enable
-If non-@code{nil}, allow glyphs to appear on displays where they are supported.
+@deffn{User Option} widget-image-enable
+If non-@code{nil}, allow images to appear on displays where they are supported.
 @end deffn