Oh dear. I regret to inform you that commit 62f29fda90cf1d5a1899f57ef78452471c707fd6 might be unfortunate

[Tom Tromey]

>>>>> "gdb-buildbot" == gdb-buildbot  <gdb-buildbot@sergiodj.net> writes:

gdb-buildbot> 	Highlight source code using GNU Source Highlight
gdb-buildbot> 	62f29fda90cf1d5a1899f57ef78452471c707fd6

I fixed this.
It's possible that there will be other failures -- while I tested everything
locally (obviously forgetting the no-source-highlight case), one never
can be sure -- and if there are I will fix them tomorrow.

Tom