Revision 148b67de3a7b6a030d503db45220c2e15f6ba31e

Committed on 04/12/2023 6:06 am by Luca Realdi <[email protected]> [GitHub Diff]

Avoid fatal error