summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorCarsten Dominik <carsten.dominik@gmail.com>2010-10-29 06:02:15 +0200
committerCarsten Dominik <carsten.dominik@gmail.com>2010-10-29 06:02:15 +0200
commit750fdcfc9b66da5ab81494fdbbba835d72b1bd87 (patch)
tree94dc395e56f373969726fbeb2103ec4a5c3487e9
parent110b4c461090a3e069cc437f269acc1b59abf2ce (diff)
downloadorg-mode-750fdcfc9b66da5ab81494fdbbba835d72b1bd87.tar.gz
Use -f to push maint
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 7ee8d72..5af3005 100644
--- a/Makefile
+++ b/Makefile
@@ -311,7 +311,7 @@ release:
rm org-$(TAG)*.zip
rm org-$(TAG)*.tar.gz
make pushreleasetag TAG=$(TAG)
- git push origin maint
+ git push -f origin maint
git checkout master
git merge -s ours maint
UTILITIES/set-version.pl -o $(TAG)
@@ -340,7 +340,7 @@ fixrelease:
rm org-$(TAG)*.zip
rm org-$(TAG)*.tar.gz
make pushreleasetag TAG=$(TAG)
- git push origin maint
+ git push -f origin maint
git checkout master
git merge -s ours maint
UTILITIES/set-version.pl -o $(TAG)