diff --git a/Jenkinsfile b/Jenkinsfile index b1e06f6..adc9ab6 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -28,7 +28,7 @@ pipeline { [(SCHEME): { stage("${SCHEME}") { catchError(buildResult: 'SUCCESS', stageResult: 'FAILURE') { - sh "make SCHEME=${SCHEME} test-r6rs-docker" + sh "timeout 600 make SCHEME=${SCHEME} test-r6rs-docker" } } }] @@ -48,7 +48,7 @@ pipeline { [(SCHEME): { stage("${SCHEME}") { catchError(buildResult: 'SUCCESS', stageResult: 'FAILURE') { - sh "make SCHEME=${SCHEME} test-r7rs-docker" + sh "timeout 600 make SCHEME=${SCHEME} test-r7rs-docker" } } }]