Attention is currently required from: pespin.

View Change

1 comment:

• File contrib/jenkins.sh:

  • Patch Set #1, Line 7: clone_repo() {

    did you think about using pushd+popd?

    yes. IMHO it makes it more complicated since depending if the git repository exists already or not, we would need to pushd once or twice.

To view, visit change 29772. To unsubscribe, or for help writing mail filters, visit settings.