Thanks for noticing this The cause is https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=951715 and indeed I had forgotten about it: in the next few days I'll try to prepare a patch and/or ping the pygments maintainer.
-- Elena ``of Valhalla''
Thanks for noticing this The cause is https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=951715 and indeed I had forgotten about it: in the next few days I'll try to prepare a patch and/or ping the pygments maintainer.
-- Elena ``of Valhalla''