Another round of fixes for the upcoming release
Here, the most important commit is the last one which fixes a crasher. The rest is more or less cosmetics, but still worth having.
Here, the most important commit is the last one which fixes a crasher. The rest is more or less cosmetics, but still worth having.