diff --git a/.agents/scripts/publish-pages.sh b/.agents/scripts/publish-pages.sh index 0de0ab7..41e63d4 100755 --- a/.agents/scripts/publish-pages.sh +++ b/.agents/scripts/publish-pages.sh @@ -75,8 +75,12 @@ for route in index full-guide/index summary/index models/index agents/index \ [ -s "dist/$route.html" ] || fail "dist/$route.html missing or empty; refusing to publish" done -index=$(mktemp) -trap 'rm -f "$index"' EXIT +# GIT_INDEX_FILE must name a path that does not exist yet: git reads an existing +# empty file as a truncated index and dies with "index file smaller than +# expected". mktemp -d gives a private directory to put that path in. +index_dir=$(mktemp -d) +index="$index_dir/index" +trap 'rm -rf "$index_dir"' EXIT # `--force` because the repository .gitignore lists `dist`; here `dist` *is* the # work tree, so those rules would otherwise exclude everything we mean to ship. GIT_INDEX_FILE="$index" git --work-tree=dist add --all --force .