diff --git a/doc/todo/copy__47__move_support_for_pushinsteadOf_/comment_5_a44a1cf7b7a96854ac5b40507865c355._comment b/doc/todo/copy__47__move_support_for_pushinsteadOf_/comment_5_a44a1cf7b7a96854ac5b40507865c355._comment new file mode 100644 index 0000000000..a870583f75 --- /dev/null +++ b/doc/todo/copy__47__move_support_for_pushinsteadOf_/comment_5_a44a1cf7b7a96854ac5b40507865c355._comment @@ -0,0 +1,12 @@ +[[!comment format=mdwn + username="yarikoptic" + avatar="http://cdn.libravatar.org/avatar/f11e9c84cb18d26a1748c33b48c924b4" + subject="comment 5" + date="2024-11-03T14:48:03Z" + content=""" +FWIW, I keep running into this. Re + +> But: If this change were made, it would risk breaking existing working setups, that happen to have a push url that points to a different repository. + +`pushurl` could take precedence, as overwrite the `pushInsteadOf` mapped value (did not check what git's behavior in presence of both pushurl and pushInsteadOf). +"""]]