Only deploy docs if they were built

Tammo Jan Dijkemarequested to merge
fix_deploy_ci into master

This fixes pipeline errors that would occur when the build_doc stage was not carried out, but the deploy_doc stage would be triggered.

Edited by Tammo Jan Dijkema

Merge request reports