Merge pull request #780 from JulianHBuecher/docker-execution-fix
authorJérôme Benoit <jerome.benoit@piment-noir.org>
Thu, 12 Oct 2023 13:01:44 +0000 (13:01 +0000)
committerGitHub <noreply@github.com>
Thu, 12 Oct 2023 13:01:44 +0000 (13:01 +0000)
Fix for failed execution in Docker container


Trivial merge