diff options
Diffstat (limited to 'Jenkinsfile')
| -rw-r--r-- | Jenkinsfile | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Jenkinsfile b/Jenkinsfile index 63012cedaa..815e8eb0a8 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -172,6 +172,9 @@ def buildGhc(params) { ValidateSpeed=${speed} ValidateHpc=NO BUILD_DPH=NO + + # Due to #14291 + SplitSections=NO """ if (crossCompiling) { build_mk += """ |