From 2c0739fd69f2cc52e137a9329eba445917f2b61f Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Fri, 24 May 2024 12:52:26 +0100
Subject: [PATCH] github patch factory: support another URL format

---
 entities/GitHub/GitHubPatch.php | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/entities/GitHub/GitHubPatch.php b/entities/GitHub/GitHubPatch.php
index 1dfef71..fcb7ccf 100644
--- a/entities/GitHub/GitHubPatch.php
+++ b/entities/GitHub/GitHubPatch.php
@@ -30,6 +30,15 @@ static function construct($url, \Repository $repository) {
       if ($src_branch != $repository->defaultBranch())
         throw new \ValidationException("Patch is not against default branch");
     }
+    elseif (preg_match('@^https://github.com/([^/]+/[^/]+)/compare/([^:]+):([^:]+):(.+)$@', $url, $m)) {
+      $src_repo   = $m[1]; // user/repo
+      $org        = $m[2];
+      $repo       = $m[3];
+      $branch     = $m[4];
+
+      if ($src_repo != $repository->name())
+        throw new \ValidationException("Patch is not for Project's repository");
+    }
     elseif (preg_match('@^https://github.com/([^/]+)/([^/]+)/tree/(.+)$@', $url, $m)) {
       $org    = $m[1];
       $repo   = $m[2];