diff options
| -rw-r--r-- | contributing/web_pages/news.mdwn | 18 | ||||
| -rw-r--r-- | contributing/web_pages/news/merge-news | 13 |
2 files changed, 14 insertions, 17 deletions
diff --git a/contributing/web_pages/news.mdwn b/contributing/web_pages/news.mdwn index a9a33170..a9a86d75 100644 --- a/contributing/web_pages/news.mdwn +++ b/contributing/web_pages/news.mdwn @@ -107,20 +107,4 @@ For practical work that means to use the following commands: After that merge, work for the next month's news item can continue on `master-news_next`. -And since we're working in a branch anyway: Please commit often, push often and pull often! Few things would be nastier than having to do heavy merging on a news release date with little time at hand. - -PS: If you're lazy, you can just use the following shell-script to merge the news into master: - -> \#!/bin/sh -> -> \# merge into master -> git checkout master -> git pull --rebase -> git merge master-news_next -> -> \# push master -> git push origin master -> -> \# switch back to master-news_next -> git checkout master-news_next -> git pull --rebase + Arne Babenhauserheide uses a [[merge-news]] script for doing this. diff --git a/contributing/web_pages/news/merge-news b/contributing/web_pages/news/merge-news new file mode 100644 index 00000000..33c01b7b --- /dev/null +++ b/contributing/web_pages/news/merge-news @@ -0,0 +1,13 @@ +#!/bin/sh + +# merge into master +git checkout master +git pull --rebase +git merge master-news_next + +# push master +git push origin master + +# switch back to master-news_next +git checkout master-news_next +git pull --rebase |