Write 'searchindex.js' using minimal JSON separators

[jayaddison]

Feature or Bugfix

• Refactoring

Purpose

• Reduce the size of the HTML search index file (searchindex.js) without otherwise affecting the application's behaviour.

Detail

• When dumping the search index to JSON, use the documented minimal-whitespace separator configuration.

Relates

• Implements #13061.

[jayaddison]

Thanks @AA-Turner!