diff --git a/Jenkinsfile b/Jenkinsfile index 57a4d83a35..6c7e53f1f8 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -132,8 +132,10 @@ pipeline { } steps { sh 'export' - sh 'make distclean' - sh 'make clang-tidy-quiet' + retry (3) { + sh 'make distclean' + sh 'make clang-tidy-quiet' + } sh 'make distclean' } }