jenkins: shorten timeout (#1928)

2019-05-09 07:40:00 +02:00 · 2019-05-09 07:40:00 +02:00 · 03914d05c6
commit 03914d05c6
parent 29c2aba417
1 changed files with 2 additions and 2 deletions
--- a/Jenkinsfile.public
+++ b/Jenkinsfile.public
@ -6,7 +6,7 @@ pipeline {
        }
    }
    options {
-          timeout(time: 30, unit: 'MINUTES')
+          timeout(time: 10, unit: 'MINUTES')
    }
    stages {
        stage('Build') {