2 commits

Author	SHA1	Message	Date
Jonas Jenwald	0f0650f426	Generate the default_preferences.json file from AppOptions ... 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.	2019-02-14 20:40:34 +01:00
Jonas Jenwald	76250b923f	[Firefox addon] Refactor bundling of the default_preferences.json file	2018-03-16 16:46:57 +01:00