[PATCH 5/8] git-remote-mediawiki: use --force when adding notes

[Matthieu Moy <Matthieu.Moy@imag.fr>]

When notes are created to record a push, it normally doesn't exist yet.
However, when a push is interrupted and then restarted, it may happen
that a commit already has notes attached, and we want to reflect the newly
created remote revision, hence use 'git notes add -f' to override the
existing one

Signed-off-by: Matthieu Moy <Matthieu.Moy@imag.fr>
---
 contrib/mw-to-git/git-remote-mediawiki | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/mw-to-git/git-remote-mediawiki b/contrib/mw-to-git/git-remote-mediawiki
index f9c0cc6..f56f9b0 100755
--- a/contrib/mw-to-git/git-remote-mediawiki
+++ b/contrib/mw-to-git/git-remote-mediawiki
@@ -1264,7 +1264,7 @@ sub mw_push_revision {
 			}
 		}
 		unless ($dumb_push) {
-			run_git("notes --ref=$remotename/mediawiki add -m \"mediawiki_revision: $mw_revision\" $sha1_commit");
+			run_git("notes --ref=$remotename/mediawiki add -f -m \"mediawiki_revision: $mw_revision\" $sha1_commit");
 			run_git("update-ref -m \"Git-MediaWiki push\" refs/mediawiki/$remotename/master $sha1_commit $sha1_child");
 		}
 	}
-- 
1.7.11.1.30.g7e1baf9.dirty