diff options
| author | Emilio Jesus Gallego Arias | 2018-11-17 04:07:49 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-17 18:38:29 +0100 |
| commit | ac63486c422af0ab76a620a797dbd349d3b0b2c0 (patch) | |
| tree | 265b98ec8b616f1f64b49a8e98188e55f7c8d9e0 /dev/ci | |
| parent | 360fafb7781ca12e533f7ee55da6a4a4324e2a19 (diff) | |
[devtools] Small script to setup overlays automatically
This is very preliminary but you should get the idea. The script tries
to build contribs, then creates a branch and sets the remote properly
as to submit a PR.
Usage example:
```
./dev/tools/create_overlays.sh ejgallego 9999 ltac2 elpi
```
This only works for contributions hosted in github for now.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/ci-common.sh | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 7a450d0d48..a5aa54144c 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -46,8 +46,11 @@ for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null . "${overlay}" done + +set +x # shellcheck source=ci-basic-overlay.sh . "${ci_dir}/ci-basic-overlay.sh" +set -x # [git_download project] will download [project] and unpack it # in [$CI_BUILD_DIR/project] if the folder does not exist already; |