diff options
author | 2016-01-13 11:42:18 -0800 | |
---|---|---|
committer | 2016-01-13 11:42:18 -0800 | |
commit | b70206fe52ee6509f3f965bf2a95b2cbd321088d (patch) | |
tree | fa59a43171854465c89af72734d45350070b7366 /tools/jenkins/run_jenkins.sh | |
parent | 295a7ce511f1a2145f70942f826d0e225c00ba62 (diff) | |
parent | 7149ca6bd0ce73a08fa512415d3f641a06a15a75 (diff) |
Merge branch 'master' into release-0_12_master_merge
Diffstat (limited to 'tools/jenkins/run_jenkins.sh')
-rwxr-xr-x | tools/jenkins/run_jenkins.sh | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tools/jenkins/run_jenkins.sh b/tools/jenkins/run_jenkins.sh index 9b6ba71948..84b4ea51ed 100755 --- a/tools/jenkins/run_jenkins.sh +++ b/tools/jenkins/run_jenkins.sh @@ -1,5 +1,5 @@ #!/usr/bin/env bash -# Copyright 2015, Google Inc. +# Copyright 2015-2016, Google Inc. # All rights reserved. # # Redistribution and use in source and binary forms, with or without @@ -92,4 +92,3 @@ if [ "$TESTS_FAILED" != "" ] then exit 1 fi - |