From 0d07104f9721e584af38d091b85d2630baf8be69 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Nov 2019 16:25:58 +0100
Subject: [PATCH] add new projects to build-all
---
build-all | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/build-all b/build-all
index 806397c8a..6160f720c 100755
--- a/build-all
+++ b/build-all
@@ -28,11 +28,15 @@ PROJECTS = [
{ 'name': 'reloc', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'c', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'tutorial-popl18', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
+ { 'name': 'spygame', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] }, # these do not work, for some reason
+ { 'name': 'time-credits', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
+ { 'name': 'actris', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
]
for project in PROJECTS:
print("Triggering build for {}{}...".format(project['name'], '' if project['branch'] == 'master' else ':'+project['branch']))
- url = "https://gitlab.mpi-sws.org/api/v4/projects/iris%2F{}/pipeline".format(project['name'])
+ 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'])),
--
GitLab