manual: Sync manual with "org.texi"
commitc30f01418fa86180ea80ff2f43a1b9935b9d2dab
authorNicolas Goaziou <mail@nicolasgoaziou.fr>
Tue, 27 Feb 2018 18:57:55 +0000 (27 19:57 +0100)
committerNicolas Goaziou <mail@nicolasgoaziou.fr>
Tue, 27 Feb 2018 19:18:10 +0000 (27 20:18 +0100)
treee93d69b40e7264152eabb2cc80fb1fb253400316
parent3dc112d5161304477b7aa6de3071b10a9b226673
manual: Sync manual with "org.texi"

Use @samp{...} in index.
contrib/manual.org