ci: Update

This commit is contained in:
Anmol Sethi 2022-12-07 20:59:24 -08:00
parent 8f988ddbb9
commit 472c101e50
No known key found for this signature in database
GPG key ID: 25BC68888A99A8BA
2 changed files with 2 additions and 8 deletions

View file

@ -3,10 +3,4 @@ set -eu
. "$(dirname "$0")/sub/lib.sh" . "$(dirname "$0")/sub/lib.sh"
cd -- "$(dirname "$0")/.." cd -- "$(dirname "$0")/.."
if is_changed README.md; then ./ci/sub/bin/fmt.sh
sh_c tocsubst --skip 1 README.md
fi
if is_changed docs/INSTALL.md; then
sh_c tocsubst --skip 1 docs/INSTALL.md
fi
./ci/sub/fmt/make.sh

2
ci/sub

@ -1 +1 @@
Subproject commit f668611e9b1cfc335230ab6f8161cf87f74f174d Subproject commit 8892ef43000921a29a1f1118c84d7eabbb9ef0c5