On Thu, Sep 11, 2014 at 4:31 PM, James Darnley <james.darnley at gmail.com> wrote: > --- > doc/developer.texi | 6 +++--- > 1 file changed, 3 insertions(+), 3 deletions(-) I would use @command{}. [...] Timothy