diff --git a/build-all b/build-all index a96e047cdb369e02dcc25558d579b3bee2566828..eb4f0955503ece6dba906f478eb517761d65e65d 100755 --- a/build-all +++ b/build-all @@ -32,14 +32,17 @@ PROJECTS = [ { 'name': 'tutorial-popl21', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] }, ] +filter = sys.argv[1] if len(sys.argv) > 1 else '' for project in PROJECTS: - print("Triggering build for {}{}...".format(project['name'], '' if project['branch'] == 'master' else ':'+project['branch'])) - id = str(project['id']) if 'id' in project else "iris%2F{}".format(project['name']) - url = "https://gitlab.mpi-sws.org/api/v4/projects/{}/pipeline".format(id) - json = { - 'ref': project['branch'], - 'variables': list(map(lambda var: { 'key': var, 'value': os.environ.get(var, "master") }, project['vars'])), - } - r = requests.post(url, headers={'PRIVATE-TOKEN': GITLAB_TOKEN}, json=json) - r.raise_for_status() - print(" Pipeline running at {}".format(r.json()['web_url'])) + name_branch = project['name'] + ('' if project['branch'] == 'master' else ':'+project['branch']) + if filter in name_branch: + print("Triggering build for {}...".format(name_branch)) + id = str(project['id']) if 'id' in project else "iris%2F{}".format(project['name']) + url = "https://gitlab.mpi-sws.org/api/v4/projects/{}/pipeline".format(id) + json = { + 'ref': project['branch'], + 'variables': list(map(lambda var: { 'key': var, 'value': os.environ.get(var, "master") }, project['vars'])), + } + r = requests.post(url, headers={'PRIVATE-TOKEN': GITLAB_TOKEN}, json=json) + r.raise_for_status() + print(" Pipeline running at {}".format(r.json()['web_url']))