From b7002b49b70c5725baf01944b0dccc8f462de532 Mon Sep 17 00:00:00 2001
From: Wolfgang Maier <maierw@informatik.uni-freiburg.de>
Date: Wed, 5 Jun 2024 16:09:54 +0200
Subject: [PATCH] Sanitize preview before commenting

---
 github_run.py | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/github_run.py b/github_run.py
index 5c5ebf1..b15d8e2 100644
--- a/github_run.py
+++ b/github_run.py
@@ -15,6 +15,24 @@ def __init__(self):
         self.pr_number = os.getenv("PR_NUMBER")
 
     def comment(self, comment_text):
+        # Enclose mentions and hashtags in backticks before commenting
+        # so that they stand out for the reviewer and to prevent accidental
+        # mentioning of github users.
+        # When replacing mentions we explicitly handle mastodon-style ones
+        # (i.e. @user@server patterns).
+        # We deliberately leave "#"s and "@"s alone if they are following a "/"
+        # to avoid destroying links.
+        # by accident.
+        comment_text = re.sub(
+            r"([^a-zA-Z0-9_/])((?:[@][\w-]+)(?:[@][\w.-]+)?)",
+            lambda m: f"{m.group(1)}`{m.group(2)}`",
+            comment_text
+        )
+        comment_text = re.sub(
+            r"([^a-zA-Z0-9_/])([#][\w]+)",
+            lambda m: f"{m.group(1)}`{m.group(2)}`",
+            comment_text
+        )
         print(comment_text)
         if (
             not comment_text