Skip to content

Minor corrections including code modifications

As reminded here, the branch minor_corrections is not intended for removing dead code. So I'm doing a separate branch.

Merge request reports