search

agda / agda-github-syntax-highlighting

Syntax highlighting used on GitHub
MIT License
4 stars 4 forks source link

`data` not always highlighted correctly #4

Open ajrouvoet opened 3 years ago

ajrouvoet commented 3 years ago

Reporting the following highlighting error in a diff on Github:

image

where data should be orange.

andreasabel commented 3 years ago

This regex should fire: https://github.com/agda/agda-github-syntax-highlighting/blob/ba7aef428c0b900675696de17e1ee6bc9d7e684e/Agda.yml#L33-L39 Not sure why it doesn't. (The open *import looks a bit unusual.) It seems that instead this one fires: https://github.com/agda/agda-github-syntax-highlighting/blob/ba7aef428c0b900675696de17e1ee6bc9d7e684e/Agda.yml#L49-L58