Peter Barker 8ab0e67da9 .github: adjust workflow for change in github workspace path
changing the permissions seems to change the path to the workspace; use the supplied variable for what it's good for
2025-06-28 09:48:18 +09:00
..