Minor fixes

Open foxtran opened this issue 1 year ago • 0 comments

I have cherry-picked the commits which can be safely merged with devel branch.

The rest commits are still in #223

Oct 07 '24 19:10 foxtran