>> Thanks. Please apply the attached patch to `texinfo.tex` to make
>> `@setcolor` work in `@example` environments; it is necessary to
>> temporarily make a space character behave normally.
>
> Thanks a lot! I'll test it as soon as possible.
Note that the actual command to be used by 'pygments' shouldn't be
`@setcolor` but rather a texinfo macro, say, `@color`:
```
@color{<color>}{<colored text>}
```
This macro would be a no-op for the info format, and both the TeX and
HTML implementations would put the `@setcolor` command into a 'group'
so that a previous colour would be restored after calling `@color`.
Werner
