From a5ea0a9d01a9c412f908d879cc80f2496a48d79b Mon Sep 17 00:00:00 2001 From: Federico Fissore Date: Mon, 25 Aug 2014 18:00:25 +0200 Subject: [PATCH] Script used by the Jenkins Github Pull Request Builder plugin --- build/build_pull_request.bash | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100755 build/build_pull_request.bash diff --git a/build/build_pull_request.bash b/build/build_pull_request.bash new file mode 100755 index 000000000..15ea13eb0 --- /dev/null +++ b/build/build_pull_request.bash @@ -0,0 +1,26 @@ +#!/bin/bash -e + +if [ "x${ghprbPullId}" == "x" ] +then + exit 1 +fi + +ant -Djava.net.preferIPv4Stack=true -Dplatform=linux64 -Dlinux64=1 clean build test + +ERRORS=`grep '