diff --git a/build/coqdoc b/build/coqdoc index 31de37b84c5cf3be0f1c6d8d5799dd34063ce862..d3539b3df6d8bc2337e513628af161cff045bf7f 100755 --- a/build/coqdoc +++ b/build/coqdoc @@ -17,4 +17,4 @@ set -x make html # Upload documentation -rsync -a -e "$GIT_SSH" html/ "$DOCDIR/" +rsync -a --delete -e "$GIT_SSH" html/ "$DOCDIR/"