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)
commit62e6f735ac3e8c9cd3db53dc7407837232605d4b
treeabf2ed5e78c5609bf30be1939efafe2acafd653c
parent1800e3384e33703b3c27e472ca451b5e6e1ed519
parentaba7e8468ad20b22891aa25e69600f6f60431cc3
Merge branch 'build' into 'main'

Fixes to build-sh script

See merge request yarrg/jarrg!5