From edeb162c478e27fc0a6ee99396e0d8c17f462803 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 25 Jan 2018 17:31:49 +0100 Subject: [PATCH] CI docs: delete stale files --- build/coqdoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build/coqdoc b/build/coqdoc index 31de37b..d3539b3 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/" -- GitLab