From 6d356d9f833d1599a95ecf737a93d4fe7e991b74 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Aug 2022 09:22:09 -0400
Subject: [PATCH] add simuliris to iris-bot
---
iris-bot | 1 +
1 file changed, 1 insertion(+)
diff --git a/iris-bot b/iris-bot
index da76fcd6a..75ed999f5 100755
--- a/iris-bot
+++ b/iris-bot
@@ -32,6 +32,7 @@ PROJECTS = {
'spygame': { 'name': 'spygame', 'branch': 'master' },
'time-credits': { 'name': 'time-credits', 'branch': 'master' },
'actris': { 'name': 'actris', 'branch': 'master' },
+ 'simuliris': { 'name': 'simuliris', 'branch': 'master' },
'tutorial-popl20': { 'name': 'tutorial-popl20', 'branch': 'master' },
'tutorial-popl21': { 'name': 'tutorial-popl21', 'branch': 'master' },
}
--
GitLab