Commit f0480ff835ef5f1da95633b47b3dbaf86acf5a9b

Reuben Thomas 2017-12-11T14:12:19

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.