- highlight.min.js now v11.5.1 (from 10.?)
- highlight theme now agate (from an-old-hope)
- highlight font custom loads Panda Sans Code:
  - or a list of other decent fonts that might be present
  for when a browser can't deal with woff2 fonts.