chore(travis): fix package name
This commit is contained in:
parent
06899d02c0
commit
558c07738c
1 changed files with 1 additions and 1 deletions
|
@ -308,7 +308,7 @@ after_script:
|
|||
fi;
|
||||
mkdir ${UPLOAD_DIR};
|
||||
if [[ $LEANREPO == BLESSED && $PACKAGE == TRUE ]]; then
|
||||
cp -v build/*.zip ${UPLOAD_DIR}/;
|
||||
cp -v build/lean*.tar.gz ${UPLOAD_DIR}/;
|
||||
fi
|
||||
cp -v build/shell/lean ${UPLOAD_DIR}/${BINARY};
|
||||
tar cvfz ${UPLOAD_DIR}/${ARCHIVE_BINARY}.tar.gz ${UPLOAD_DIR}/${BINARY};
|
||||
|
|
Loading…
Reference in a new issue