diff options
Diffstat (limited to 'contrib/jenkins.sh')
| -rwxr-xr-x | contrib/jenkins.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/jenkins.sh b/contrib/jenkins.sh index bf755b6..5ce5993 100755 --- a/contrib/jenkins.sh +++ b/contrib/jenkins.sh @@ -9,6 +9,7 @@ fi set -e +publish="$1" base="$PWD" deps="$base/deps" inst="$deps/install" |