Skip to content

fix: restore syntax highlighting - #973

Open
ROTARTSI82 wants to merge 1 commit into
leanprover:mainfrom
ROTARTSI82:patch-1
Open

fix: restore syntax highlighting#973
ROTARTSI82 wants to merge 1 commit into
leanprover:mainfrom
ROTARTSI82:patch-1

Conversation

@ROTARTSI82

@ROTARTSI82 ROTARTSI82 commented Aug 26, 2026

Copy link
Copy Markdown

It seems pull request #954 broke syntax highlighting in message outputs (at least in the latest verso-slides)?

The entire text would be --verso-message-info-color and would default to black:
Image

I used an LLM to find and write this fix, and in conjunction with a patch to verso-slides (verso-slides#71) to use the new CSS variables, this restores the old behavior:
image

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant