diff --git a/tools/jenkins/run_jenkins.sh b/tools/jenkins/run_jenkins.sh index 67cfc2bb0a4..0e1af2a2a9a 100755 --- a/tools/jenkins/run_jenkins.sh +++ b/tools/jenkins/run_jenkins.sh @@ -86,3 +86,9 @@ else echo "Unknown platform $platform" exit 1 fi + +if [ ! -e reports/index.html ] +then + mkdir -p reports + echo 'No reports generated.' > reports/index.html +fi