domi/forgejo-domi
1
0
Fork 0
forked from forgejo/forgejo
Code Pull requests Activity

Abort merge if head has been updated before pressing merge (#18032)

Browse source 
* Abort merge if head has been updated before pressing merge

It is possible that a PR head may be pushed to between the merge page being shown
and the merge button being pressed. Pass the current expected head in as a parameter
and cancel the merge if it has changed.

Fix #18028

Signed-off-by: Andrew Thornton <art27@cantab.net>

* adjust swagger

Signed-off-by: Andrew Thornton <art27@cantab.net>

* fix test

Signed-off-by: Andrew Thornton <art27@cantab.net>

* placate lint

Signed-off-by: Andrew Thornton <art27@cantab.net>
This commit is contained in:
zeripath 2021-12-20 00:32:54 +00:00 • committed by GitHub
parent b24a965b81
commit e4e411821d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
9 changed files with 42 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

1
options/locale/locale_en-US.ini
View file

@ -1506,6 +1506,7 @@ pulls.rebase_conflict_summary = Error Message
; </summary><code>%[2]s<br>%[3]s</code></details>
pulls.unrelated_histories = Merge Failed: The merge head and base do not share a common history. Hint: Try a different strategy
pulls.merge_out_of_date = Merge Failed: Whilst generating the merge, the base was updated. Hint: Try again.
pulls.head_out_of_date = Merge Failed: Whilst generating the merge, the head was updated. Hint: Try again.
pulls.push_rejected = Merge Failed: The push was rejected. Review the githooks for this repository.
pulls.push_rejected_summary = Full Rejection Message
pulls.push_rejected_no_message = Merge Failed: The push was rejected but there was no remote message.<br>Review the githooks for this repository