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



Reply via email to