diff --git a/jenkins b/jenkins index 60eddfe68..915aefd9d 100755 --- a/jenkins +++ b/jenkins @@ -5,8 +5,20 @@ echo "starting build..." if [ "$?" = "0" ]; then echo "build succeeded" - - echo "TODO: build debian package" + + if [ ! -z "$PACKAGE" ]; then + echo "publishing ubuntu package (.deb)" + DEBPATH=`find target/deb -name *.deb` + DEBNAME=`basename $DEBPATH` + + curl -f -T $DEBPATH $DEB_SERVER/$DEBNAME + + if [ "$?" != "0" ]; then + echo "deb publish failed" + exit 1 + fi + echo "done publishing deb" + fi else echo "build failed" exit 1