|
From: Raymond T. <toy...@gm...> - 2025-07-10 15:11:05
|
On 7/8/25 9:00 AM, Leo Butler wrote: > On Mon, Jul 07 2025, Jaime Villate via Maxima-discuss<max...@li...> wrote: >> >> Sure, look at the attachment. > I don't think the fault is with syntax highlighting, but rather an > incomplete list of symbols. > > Failing an improved list, it would be worth figuring out how to add a > widget to the web pages that disables syntax highlighting. The highligter is written in Javascript, so we definitely could in principle. I'm not really sure how to integrate that with all the stuff that is autogenerated by makeinfo. ​ |