diff --git a/services/web/app/src/Features/Compile/ClsiManager.mjs b/services/web/app/src/Features/Compile/ClsiManager.mjs index 8b9a9ed6e7..cb2502bc99 100644 --- a/services/web/app/src/Features/Compile/ClsiManager.mjs +++ b/services/web/app/src/Features/Compile/ClsiManager.mjs @@ -1114,7 +1114,7 @@ async function _getContentFromMongo(projectId) { function _finaliseRequest(projectId, options, project, docs, files) { const resources = [] - let flags + let flags = [] let rootResourcePath = options.rootResourcePath let rootResourcePathOverride = null let hasMainFile = false @@ -1182,9 +1182,13 @@ function _finaliseRequest(projectId, options, project, docs, files) { if (options.fileLineErrors) { flags = ['-file-line-error'] } + if (process.env.TEX_COMPILER_EXTRA_FLAGS) { + flags.push(...process.env.TEX_COMPILER_EXTRA_FLAGS.split(/\s+/).filter(Boolean)) + } const hasPremiumCompiles = ['alpha', 'priority'].includes( options.compileGroup ) + return { compile: { options: {