diff --git a/tools/jenkins/run_jenkins.sh b/tools/jenkins/run_jenkins.sh index 67cfc2bb0a4a839d93a8c53feb1cfc234e9ab724..0e1af2a2a9a94702a529645139ad418dd4edec64 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