From ebef67b3549d8612cbece0e8a3b3355a41c80fdf Mon Sep 17 00:00:00 2001 From: Jonas Jenwald Date: Sat, 21 Mar 2020 12:53:20 +0100 Subject: [PATCH] Stop building any `src/` files during the `gulp default_preferences` task With the changes made in the previous patch, the `web/app_options.js` file no longer depends on anything *except* files residing in the `web/` folder. Hence the `gulp default_preferences` task can now be further simplified and thus becomes even faster than before; see also PR 11724. --- gulpfile.js | 8 -------- 1 file changed, 8 deletions(-) diff --git a/gulpfile.js b/gulpfile.js index 18a2ab9fa..120d4fdba 100644 --- a/gulpfile.js +++ b/gulpfile.js @@ -563,14 +563,6 @@ gulp.task("default_preferences-pre", function () { }; var preprocessor2 = require("./external/builder/preprocessor2.js"); return merge([ - gulp.src( - [ - "src/{display,shared}/*.js", - "!src/shared/{cffStandardStrings,fonts_utils}.js", - "src/pdf.js", - ], - { base: "src/" } - ), gulp.src(["web/{app_options,viewer_compatibility}.js"], { base: ".", }),