Synchronize master branch with 2024-patches
No change WRT master, but it records a merge commit to simplify future synchronization.
Edited by Marco Clemencic
No change WRT master, but it records a merge commit to simplify future synchronization.