1f1ad09e38
The preceding commit, which made docs/highlighters.md and highlighters/README.md distinct, allows reverting their removal.