From 34dc9f42d48889b37b2ef301bf708322def5bae6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 6 Sep 2021 14:12:07 -0400
Subject: [PATCH] explain why only Iris timing can be diff'd
---
iris-bot | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/iris-bot b/iris-bot
index 7184f2c79..b166d9094 100755
--- a/iris-bot
+++ b/iris-bot
@@ -92,6 +92,10 @@ def build(args):
def time(args):
# Make sure only 'iris' variables are set.
+ # One could imagine generalizing to "either Iris or std++", but then if the
+ # ad-hoc timing jobs honor STDPP_REV, how do we make it so that particular
+ # deterministic std++ versions are used for Iris timing? This does not
+ # currently seem worth the effort / hacks.
for project in BUILD_BRANCHES.keys():
if project != 'iris':
print("'time' command only supports Iris branches")
--
GitLab