From c3ef007227d0e9019e6f0d5151b2f464eeb6bf37 Mon Sep 17 00:00:00 2001
From: FinnStutzenstein <finn.stutzenstein@hotmail.de>
Date: Tue, 17 Apr 2018 15:23:15 +0200
Subject: [PATCH] Fixed IE11 Error in pdfjs-dist

---
 gulpfile.js | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/gulpfile.js b/gulpfile.js
index 12432640a..8568daa21 100644
--- a/gulpfile.js
+++ b/gulpfile.js
@@ -64,6 +64,8 @@ gulp.task('js-libs', function () {
         .pipe(sourcemaps.write())
         .pipe(inject.prepend("/* set basepath of CKEditor */\n" +
                 "window.CKEDITOR_BASEPATH = '/static/ckeditor/';\n\n"))
+        .pipe(inject.prepend("/* Workaround for IE and pdfjs-dist#1.3.100 (see PR#3714) */\n" +
+                "PDFJS = {workerSrc: 'not used but set'};\n\n"))
         .pipe(gulpif(argv.production, uglify()))
         .pipe(gulp.dest(path.join(output_directory, 'js')));
 });