Jim, Eric, > Wouldn't @command be better than @samp?
Yes, sure. You're right. Committed. http://git.sv.gnu.org/gitweb/?p=gnulib.git;a=commitdiff;h=7bfb1880ea713532edaaed3386bc0a2ba45a28a6 Bruno
Jim, Eric, > Wouldn't @command be better than @samp?
Yes, sure. You're right. Committed. http://git.sv.gnu.org/gitweb/?p=gnulib.git;a=commitdiff;h=7bfb1880ea713532edaaed3386bc0a2ba45a28a6 Bruno