Skip to content

Add additional headers; fix names of workflows

Wouter Deconinckrequested to merge
github-actions into main

More changes for GitHub.

Merge request reports