diff --git a/.ci/checkgithistory.sh b/.ci/checkgithistory.sh index 82b0a4bc2..07f63007e 100755 --- a/.ci/checkgithistory.sh +++ b/.ci/checkgithistory.sh @@ -1,10 +1,16 @@ #!/bin/sh +set -e + +# the script checks if the public repo and the local repo commit history are sync, otherwise it fails +if [ $# -ne 2 ]; then + >&2 echo "Not enough argument supplied. Usage: checkgithistory.sh public_url develop_branch_name" + exit 1 +fi -# the script check if the public repo and the local repo commit history are sync, otherwise it fail cd src/franka_ros -public_url="https://github.com/frankaemika/franka_ros.git" +public_url=$1 public_remote_name=$(git remote -v | grep ${public_url} | head -n 1 | sed -e 's/\s.*$//') -develop_branch_name="develop" +develop_branch_name=$2 if [ -z "$public_remote_name" ]; then public_remote_name="public" diff --git a/Jenkinsfile b/Jenkinsfile index 4fcde704c..a1d4a4dfd 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -69,7 +69,7 @@ node ('docker'){ } stage("Check public/local commit history sync") { sh """ - src/franka_ros/.ci/checkgithistory.sh + src/franka_ros/.ci/checkgithistory.sh https://github.com/frankaemika/franka_ros.git develop """ } } catch (e) {