diff options
Diffstat (limited to 'build-aux/Jenkinsfile.full')
| -rw-r--r-- | build-aux/Jenkinsfile.full | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/build-aux/Jenkinsfile.full b/build-aux/Jenkinsfile.full index 7d089f811..328812ced 100644 --- a/build-aux/Jenkinsfile.full +++ b/build-aux/Jenkinsfile.full @@ -275,16 +275,14 @@ pipeline { // TODO find a way to avoid setting this explicitly spidermonkey = '78' } - options { - // TODO start this timeout _after_ the agent has been acquired if possible - timeout(time: 15, unit: "MINUTES") - } steps { - sh (script: 'rm -rf apache-couchdb-*', label: 'Clean workspace of any previous release artifacts' ) - sh "./configure --spidermonkey-version ${spidermonkey}" - sh 'make erlfmt-check' - sh 'make elixir-check-formatted' - sh 'make dist' + timeout(time: 15, unit: "MINUTES") { + sh (script: 'rm -rf apache-couchdb-*', label: 'Clean workspace of any previous release artifacts' ) + sh "./configure --spidermonkey-version ${spidermonkey}" + sh 'make erlfmt-check' + sh 'make elixir-check-formatted' + sh 'make dist' + } } post { success { |