UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
222 stars 71 forks source link

Fail the website build on unparsed concept macro invocations #1066

Closed VojtechStep closed 8 months ago

VojtechStep commented 8 months ago

I found two instances where the concepts macro wasn't formatted properly, so I added a check to the preprocessor that fails the website build.

This means that the preprocessor will run in full for the linkcheck output. We could have it only do some of the work for just checking if all the tags are well-formatted, but most of the time is still spent in IO with the mdbook process, which we can't speed up.