CI pipeline improvements
add options to avoid building documentation at each commit, to choose draft mode and to select which manual (oce/ice/bgc) to build
add options to avoid building documentation at each commit, to choose draft mode and to select which manual (oce/ice/bgc) to build