This change was necessary to adapt to updates of the PDF.js version
shipped with newer FF releases.

There were three small changes. Our code now works with both
the old version (currently used with Chrome) and the old version
(embedded in FF).