From 29ee2590d4eb468ca3e338ced9ac7f7d08d0b6c5 Mon Sep 17 00:00:00 2001
From: Jonas Jenwald <jonas.jenwald@gmail.com>
Date: Sat, 21 Mar 2020 11:34:32 +0100
Subject: [PATCH] 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 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/gulpfile.js b/gulpfile.js
index 16760555d..cf697257f 100644
--- 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: ".",
     }),
   ])