Force adding of doc files in the release-doc rule

diff --git a/Makefile b/Makefile
index da9a74304ef29e7cc580c4eb55e63c5eeae70e57..69668d46275a2fcef88f7bcead7a22580ba9c8f8 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -113,7 +113,7 @@ release-doc:
        git checkout release && \
        git merge master && \
        $(MAKE) clean doc-man doc-html && \
-       git add $(MANDOC) $(HTMLDOC) && \
+       git add -f $(MANDOC) $(HTMLDOC) && \
        git commit -m "Sync docs" && \
        git checkout master