From d13434481cb1fc047bb6f6f180dccc8f9656a2a7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 2 May 2023 14:49:23 +0200
Subject: [PATCH] iris-bit: print markdown link for timing results
---
iris-bot | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/iris-bot b/iris-bot
index 8f2b36114..96c7e19b4 100755
--- a/iris-bot
+++ b/iris-bot
@@ -140,7 +140,9 @@ def time(args):
else:
test_pipeline = trigger_build(project['name'], args.test_rev, vars)
print(" Test pipeline (on non-standard branch {}) running at {}".format(args.test_rev, test_pipeline['web_url']))
- print(" Once done, timing comparison will be available at https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project={}&var-branch1=@hoc&var-commit1={}&var-config1={}&var-branch2=@hoc&var-commit2={}&var-config2={}".format(project['name'], base_pipeline['sha'], id+"-base", test_pipeline['sha'], id+"-test"))
+ url = "https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project={}&var-branch1=@hoc&var-commit1={}&var-config1={}&var-branch2=@hoc&var-commit2={}&var-config2={}".format(project['name'], base_pipeline['sha'], id+"-base", test_pipeline['sha'], id+"-test")
+ print(" Once done, timing comparison will be available at {}".format(url))
+ print(" Markdown link: [{}]({})".format(project_name, url))
# Dispatch
if __name__ == "__main__":
--
GitLab