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-11T14:12:19