diff options
| -rwxr-xr-x | tools/jenkins/run_jenkins.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tools/jenkins/run_jenkins.sh b/tools/jenkins/run_jenkins.sh index 67cfc2bb0a..0e1af2a2a9 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 |