This is needed to generate PDF user manual without typesetting
artifacts.
Change-Id: Ibcbd804dac2b9415459327f53f6fad0dc38fa5c6
Signed-off-by: Paul Fertser <fercerpav@gmail.com>
Reviewed-on: http://openocd.zylin.com/3919
Tested-by: jenkins
Reviewed-by: Andreas Fritiofson <andreas.fritiofson@gmail.com>