Merge pull request ghostty-org#178 from 00-kat/very-useful

A simply essential feature
00-kat · Mar 7, 2025 · 891fc87 · 891fc87
2 parents 44dfe96 + d109328
commit 891fc87
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/app/components/entity_mentions/resolution.py b/app/components/entity_mentions/resolution.py
@@ -48,6 +48,9 @@ async def resolve_repo_signatures(content: str) -> AsyncIterator[tuple[str, str,
             case None, "main" | "web" | "bot" as repo:
                 # Special ghostty-org prefixes
                 yield config.GITHUB_ORG, config.GITHUB_REPOS[repo], number
+            case None, "bobr":
+                # A touch of personalization
+                yield config.GITHUB_ORG, config.GITHUB_REPOS["bot"], number
             case None, repo:
                 # Only a name provided, e.g. uv#8020.
                 with suppress(RequestFailed, RuntimeError):