Fix the documentation-* jobs, and add SSH publisher
Change-Id: Ie28cf03be5ad62d49c80e4c83b4d58a97226c4af
diff --git a/jjb/shell/repopatch.sh b/jjb/shell/repopatch.sh
index 93c9706..4e38e66 100644
--- a/jjb/shell/repopatch.sh
+++ b/jjb/shell/repopatch.sh
@@ -17,17 +17,23 @@
# repopatch.sh
# downloads a patch to within an already checked out repo tree
-set +e -u -o pipefail
+set -eu -o pipefail
# verify that we have repo installed
command -v repo >/dev/null 2>&1 || { echo "repo not found, please install it" >&2; exit 1; }
-echo "Checking out patch with repo, using repo version:"
-repo version
-
+echo "DESTINATION_DIR: ${DESTINATION_DIR}"
echo "GERRIT_PROJECT: ${GERRIT_PROJECT}"
echo "GERRIT_CHANGE_NUMBER: ${GERRIT_CHANGE_NUMBER}"
echo "GERRIT_PATCHSET_NUMBER: ${GERRIT_PATCHSET_NUMBER}"
-echo "Make this work eventually!"
+pushd "${DESTINATION_DIR}"
+echo "Checking out a patchset with repo, using repo version:"
+repo version
+
+PROJECT_PATH=$(xmllint --xpath "string(//project[@name=\"${GERRIT_PROJECT}\"]/@path)" .repo/manifest.xml)
+echo "Project Path: $PROJECT_PATH"
+
+repo download "${PROJECT_PATH}" "$GERRIT_CHANGE_NUMBER/${GERRIT_PATCHSET_NUMBER}"
+popd