rebuild lean.min.js

[eric-wieser]

An upstream change meant that the previous build no longer works.
The build tool was changed upstream to make this work again in highlightjs/highlight.js@76efccf.

This probably means that the new build will stop working on previous versions, but I doubt we can do much about that.

[bryangingechen]

Do you know roughly which versions will stop working? It might be good to add a warning in the README regarding compatibility.

[eric-wieser]

No, I'm afraid I have no idea at all.

[bryangingechen]

I'm assuming you built this following the directions in the README, which involve cloning highlightjs? In hindsight, those instructions weren't very stable, since highlightjs master could (and did) end up incompatible with highlightjs-lean.

I'm thinking I should probably do the following:

1. release a v11-compatible highlightjs-lean v2
2. pin a compatible version of highlightjs in the build instructions in the README / the GitHub actions workflow
3. add a note in the README pointing users of earlier versions of highlightjs to highlightjs-lean v1

[eric-wieser]

I'm assuming you built this following the directions in the README, which involve cloning highlightjs? I

This is just the version that CI built for us, which AFAIR does follow those instructions.