Push GDAL docset directly from official repo

[ThomasG77]

Hello,

I'm using Zeal to work offline sometimes and GDAL doc is outdated e.g version 1.11.1 (see https://zealusercontributions.vercel.app/search?q=gdal and repo https://github.com/Kapeli/Dash-User-Contributions/tree/master/docsets/GDAL) while latest GDAL is 3.6.0 e.g old GDAL docset XML for Dash/Zeal

To submit, https://github.com/Kapeli/Dash-User-Contributions#readme

Recipe to build the docset

git clone https://github.com/OSGeo/gdal.git
cd gdal
git checkout v3.6.0
mkdir -p doc/build
doxygen Doxyfile
cd doc
make html O="-D enable_redirects=1"
cd ..
python -m pip install doc2dash
doc2dash \
    --index-page index.html \
    --icon doc/images/gdalicon.png \
    --online-redirect-url https://gdal.org/ \
    doc/build/html
tar --exclude='.DS_Store' -cvzf GDAL.tgz GDAL.docset
cd ..

# Forked repo of official one to submit the new doc
git clone https://github.com/<youruser>/Dash-User-Contributions
cd Dash-User-Contributions
git checkout -b gdal-docset-v3.6.0
cd docsets/GDAL/
cp ../../../gdal/GDAL.tgz .
echo '{
    "name": "GDAL",
    "version": "3.6.0",
    "archive": "GDAL.tgz",
    "author": {
        "name": "GDAL",
        "link": "https://twitter.com/GdalOrg"
    },
    "aliases": ["GDAL", 
                "Geospatial Data Abstraction Library"],
}' >| docset.json
# Then open PR on official repo

PS: I could submit an update myself but I think it would be better to integrate docset publication in the official repo building workflow

[rouault]

If you update mkgdaldist.sh and HOWTO-RELEASE to automate this in a no-brainer fashion for the release manager, why not? Everything must be explained down-to-Earth, with PR text ready to be copied&pasted, because thinking is not option when doing a release :-) Actually this should perhaps not be in mkgdaldist.sh which is used at release candidate generation time, but in a new script run after the release candidate has been approved To be honest, as I didn't know what Zeal is (which doesn't prove necessarily a lot), I'm wondering how useful that would be to other users to justify the extra burden on the release manager. Ideally we'd want this to be a 0-cost operation for the release manager, and thus fully automated as a github action workflow, triggered on a github release, but that would involve passing some credentials and use github API to automate the PR creation. I'd very favorable to this if you want to set it up.