Closed lovettchris closed 2 years ago
sync the latest highlight.js from lean4.
There is a conflict. Could you try to produce cleaner commit histories, preferably without merge commits?
Can you just use this squash merge feature?
sync the latest highlight.js from lean4.