From ac63486c422af0ab76a620a797dbd349d3b0b2c0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 17 Nov 2018 04:07:49 +0100
Subject: [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.
---
 dev/ci/ci-common.sh | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'dev/ci')

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;
-- 
cgit v1.2.3