assets: Use temporarily a patched highlightjs-line-numbers library

There is an annoying copy / paste behavior with browsers different from
chromium, so use a patched version of the library fixing it.

Pull request has been submitted to the library author,
see https://github.com/wcoder/highlightjs-line-numbers.js/issues/51