Merge pull request #11724 from Snuffleupagus/default_preferences-web-files

Only build the necessary `web/` files during the `gulp default_preferences` task
2020-03-22 16:30:56 +01:00 · 2020-03-22 16:30:56 +01:00 · 066ff62527
commit 066ff62527
parent f53db81c20 29ee2590d4
1 changed files with 1 additions and 1 deletions
--- a/gulpfile.js
+++ b/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: ".",
    }),
  ])