Check if directories exist on the remote DAV server before deleting them

gitlab/before_docs.sh

@@ -18,9 +18,9 @@ fi
 
 # prefix differs between private & public repos
 if [[ "${VISIBILITY}" == "public" ]]; then
-  DOCS_SERVER_PREFIX="public-upload/$CI_PROJECT_PATH/docs/"
+  DOCS_SERVER_PREFIX="public-upload/$CI_PROJECT_PATH/docs"
 else
-  DOCS_SERVER_PREFIX="private-upload/$CI_PROJECT_PATH/docs/"
+  DOCS_SERVER_PREFIX="private-upload/$CI_PROJECT_PATH/docs"
 fi
 
 # define possible upload paths

gitlab/functions.sh

@@ -204,9 +204,17 @@ dav_mkdir() {
 # Deletes a file/folder from our intranet location via curl
 # $1: Path to the file/folder to delete (e.g. dist/myfile.whl)
 dav_delete() {
-  log_info "curl: DELETE ${1}..."
+  log_info "curl: EXISTS ${1}?"
+
+  # checks if the directory exists before trying to remove it (use --head)
+  local code=$(curl --location --silent --fail --write-out "%{http_code}" --head --user "${DOCUSER}:${DOCPASS}" "$1")
+  if [[ ${code} == *404 ]]; then
+    log_info "Directory $1 does not exist. Skipping deletion"
+    return 0
+  fi
 
-  local code=$(curl --location --silent --fail --write-out "%{http_code}" --user "${DOCUSER}:${DOCPASS}" -X DELETE "$1")
+  log_info "curl: DELETE ${1}..."
+  code=$(curl --location --silent --fail --write-out "%{http_code}" --user "${DOCUSER}:${DOCPASS}" -X DELETE "$1")
 
   if [[ ${code} == *204 || ${code} == *201 ]]; then
     log_info "Successfully deleted ${1} with curl"