0f0650f426
Currently any editing of the preferences require updates in *three* separate files, which isn't a great developer experience to say the least. This has annoyed me sufficiently to write this patch, which moves the definition of all preferences into `AppOptions` and adds a new `gulp` task to generate the `default_preferences.json` file for the builds where it's needed.
This is the PDF.js project output, https://github.com/mozilla/pdf.js Current extension version is: PDFJSSCRIPT_VERSION Taken from upstream commit: PDFJSSCRIPT_COMMIT