diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-26 20:20:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-26 20:20:33 +0200 |
| commit | 71557d5499fcf78d023eefc8d7a2b7a118b81ed5 (patch) | |
| tree | a54a50a8b7758823709ee776b4825702e3003dcf /dev/ci | |
| parent | ac2c4bc19afe7d68918cbc6f605a9bcfcdbf0f35 (diff) | |
| parent | 5a564f986b5dcb74e347fbdc571d9e1a9980c2a4 (diff) | |
Merge PR #7543: [ide] Move common protocol library to its own folder/object.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/06859-ejgallego-stm+top.sh | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh index ca0076b46..b22ab3630 100644 --- a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh +++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh @@ -1,6 +1,9 @@ #!/bin/sh -if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || [ "$CI_BRANCH" = "pr-6859" ]; then +if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || \ + [ "$CI_PULL_REQUEST" = "7543" ] || [ "$CI_BRANCH" = "ide+split" ] ; then + pidetop_CI_BRANCH=stm+top pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git + fi |