--- a/ChangeLog	Mon Dec 11 14:08:40 2017 +0100
+++ b/ChangeLog	Mon Dec 11 14:12:19 2017 +0100
@@ -1,3 +1,9 @@
+2017-12-11  Reuben Thomas  <rrt@sc3d.org>
+
+	doc: Use better texinfo tags in a few cases.
+	* doc/gnulib.texi (Extending Gnulib): Use @option or @command
+	instead of @samp in a few places.
+
 2017-12-11  Bruno Haible  <bruno@clisp.org>
 
 	unistr/base: Update comment.

--- a/doc/gnulib.texi	Mon Dec 11 14:08:40 2017 +0100
+++ b/doc/gnulib.texi	Mon Dec 11 14:12:19 2017 +0100
@@ -686,21 +686,21 @@
 You can also add unstructured amounts of code to the library, by
 grouping the non-Gnulib files of the library in a single kitchen-sink
 ``module.''  (This kind of kitchen-sink module is not needed when you
-use the @command{gnulib-tool} option @samp{--makefile-name}.)
+use the @command{gnulib-tool} option @option{--makefile-name}.)
 @end itemize
 
 In a release tarball, you can distribute the contents of this
 @option{--local-dir} directory that will be combinable with newer
 versions of Gnulib, barring incompatible changes to Gnulib.
 
-If the @samp{--local-dir=@var{directory}} option is specified, then
+If the @option{--local-dir=@var{directory}} option is specified, then
 @command{gnulib-tool} looks in @file{@var{directory}} whenever it
 reads a file from the Gnulib directory.  Suppose @command{gnulib-tool}
 is looking for @var{file}.  Then:
 
 @itemize @bullet
 @item
-If @file{@var{directory}/@var{file}} exists, then @samp{gnulib-tool} uses
+If @file{@var{directory}/@var{file}} exists, then @command{gnulib-tool} uses
 it instead of the file included in Gnulib.
 
 @item