chiark / gitweb /
Merge branch 'build' into 'main'
authorIan Jackson <ywiivi@fyvzl.net>
Sun, 9 Apr 2023 09:40:59 +0000 (09:40 +0000)
committerIan Jackson <ywiivi@fyvzl.net>
Sun, 9 Apr 2023 09:40:59 +0000 (09:40 +0000)
Fixes to build-sh script

See merge request yarrg/jarrg!5


Trivial merge