projects
/
maintainer-tools.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
bed63ed
)
github-merge-pr: doc: Install extra git-filter-repo
author
Hauke Mehrtens
<hauke@hauke-m.de>
Sat, 6 Jul 2024 16:07:25 +0000
(18:07 +0200)
committer
Christian Marangi
<ansuelsmth@gmail.com>
Tue, 16 Jul 2024 17:09:38 +0000
(19:09 +0200)
The git filter-repo command is not available by default.
Signed-off-by: Hauke Mehrtens <hauke@hauke-m.de>
github-merge-pr.sh
patch
|
blob
|
history
diff --git
a/github-merge-pr.sh
b/github-merge-pr.sh
index f294c850c963ed35f80dc21bb8eca9a632d0c62e..1bd3e2f0b072146f66a42fb7142817edcc9e078d 100755
(executable)
--- a/
github-merge-pr.sh
+++ b/
github-merge-pr.sh
@@
-6,6
+6,8
@@
# 2. Make sure you can correctly push and force push to the github
# repository
#
+# Make sure to install the extra git-filter-repo package.
+#
# Usage: github-merge-pr.sh PR_NUMBER BRANCH REPO_NAME
#
# BRANCH is optional and defaults to main.