Publish documentation on push to develop branch

[nlohmann]

Changes

• add workflow to publish documentation on push to develop branch
• minor changes:
  • make sure bash is used in docset Makefile (not needed here, but calling the Makefile in GitHub actions yielded errors, because /bin/sh was used as default shell)
  • bump version of plantuml-markdown package

Notes

The concurrency setting make sure that no two jobs of the workflow run concurrently. Jobs are waiting until previous jobs complete:

[coveralls]

Coverage remained the same at 100.0% when pulling ff108a3 on documentation_update into 2ac7d02 on develop.

[falbrechtskirchinger]

• make sure bash is used in docset Makefile (not needed here, but calling the Makefile in GitHub actions yielded errors, because /bin/sh was used as default shell)

FYI, /bin/sh is symlinked to dash on Ubuntu.

[nlohmann]

FYI, /bin/sh is symlinked to dash on Ubuntu.

Alright. It still did not work. I was trying to have an up-to-date docset somewhere, but the artifacts of GitHub are not too useful here.

[falbrechtskirchinger]

Looks good to me.