As explained in
https://github.com/mozilla/pdf.js/issues/6174#issuecomment-118502802.
To verify that this patch works:
1. Build the Chrome extension (node make chromium)
2. Load the Chrome extension (at chrome://extensions)
3. Visit https://robwu.nl/pdfjs/issue6174/.
4. Verify that PDF.js is not used to load the PDF. Either Chrome's
default PDF Viewer is used, or the PDF is offered as a file download.