#4925 Don't use @code inside of @example

[David Kastrup]

Don't use @code inside of @example

@example is already set in monospace font (use @display if you don't
want to change fonts). This replacement was done mechanically using
the script

sed -i '/@example *$/,/@end example *$/{s/@code{\(\([^@}]\|@[@{}]\)*\)}/\1/g;s/ \+$//;}' $(git grep -l '^@end example$' Documentation)

so not all replacements are really formatted best. But overall this
looks like an improvement.

http://codereview.appspot.com/304810043

[Anonymous]

Passes make, make check and a full make doc.

[Anonymous]

Patch on countdown for July 14th.

[Anonymous]

Patch counted down - please push

[David Kastrup]

Pushed to staging as
commit db92af51a444062c8edaef3afa36f57375b8feeb
Author: David Kastrup dak@gnu.org
Date: Fri Jul 8 21:41:54 2016 +0200

Issue 4925: Don't use @code inside of @example

@example is already set in monospace font (use @display if you don't
want to change fonts).  This replacement was done mechanically using
the script

    sed -i '/@example *$/,/@end example *$/{s/@code{\(\([^@}]\|@[@{}]\)*\)}/\1/g;s/ \+$//;}' $(git grep -l '^@end example$' Documentation)

so not all replacements are really formatted best.  But overall this
looks like an improvement.