Remove the gulp extension build target

[Snuffleupagus]

After PR #9566, the gulp extension build target is now basically just an alias for gulp chromium; see

pdf.js/gulpfile.js

Line 416 in e39541a

gulp.task('extension', ['chromium']);

Hence it seems, at least to me, that the gulp extension build target could simply be removed now.

---

Note that it's currently used at one other spot in gulpfile.js, see

pdf.js/gulpfile.js

Line 911 in e39541a

gulp.task('web-pre', ['generic', 'extension', 'jsdoc']);

That line can actually be simplified to just gulp.task('web-pre', ['generic', 'jsdoc']);, since the Chromium extension isn't included in the gh-pages branch and building it is thus a waste of time/resources in that case.

[Snuffleupagus]

And apparently I should have looked through gulpfile.js a bit closer before opening the issue, since these lines can be removed as well:

pdf.js/gulpfile.js

Lines 1092 to 1093 in 5053d02

	gulp.src(CHROME_BUILD_DIR + '*.crx')
	.pipe(gulp.dest(GH_PAGES_DIR + EXTENSION_SRC_DIR + 'chromium/')),

Please note: Ever since PR #8315, where support for outputting a packed Chromium extension was removed, those lines (in addition to the gulp web-pre task mentioned above) have been unused.