Only build the necessary web/ files during the gulp default_preferences task

By explicitly specifying only the required `web/` files, the runtime of the gulp task is reduced by approximately 30 percent.

gulpfile.js

@@ -602,7 +602,7 @@ gulp.task("default_preferences-pre", function() {
       ],
       { base: "src/" }
     ),
-    gulp.src(["web/*.js", "!web/{app,pdfjs,preferences,viewer}.js"], {
+    gulp.src(["web/{app_options,viewer_compatibility}.js"], {
       base: ".",
     }),
   ])