Skip to content

Commit

Permalink
Apply suggestions from code review
Browse files Browse the repository at this point in the history
Co-authored-by: Kate <[email protected]>
  • Loading branch information
rjbou and kit-ty-kate authored Oct 17, 2024
1 parent 1fc2b16 commit ca88893
Showing 1 changed file with 10 additions and 10 deletions.
20 changes: 10 additions & 10 deletions .github/scripts/main/main.sh
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ unset-dev-version () {
export OCAMLRUNPARAM=b

(set +x ; echo -en "::group::build opam\r") 2>/dev/null
if [[ $OPAM_TEST -eq 1 ]] || [[ $OPAM_DOC -eq 1 ]] ; then
if [[ "$OPAM_TEST" -eq 1 ]] || [[ "$OPAM_DOC" -eq 1 ]] ; then
export OPAMROOT=$OPAMBSROOT
# If the cached root is newer, regenerate a binary compatible root
opam env || { rm -rf $OPAMBSROOT; init-bootstrap; }
Expand Down Expand Up @@ -48,14 +48,14 @@ make install
export PATH="$PREFIX/bin:$PATH"
opam --version

if [[ $OPAM_DOC -eq 1 ]]; then
if [[ "$OPAM_DOC" -eq 1 ]]; then
make -C doc html man-html pages

if [ "$GITHUB_EVENT_NAME" = "pull_request" ]; then
. .github/scripts/common/hygiene-preamble.sh
diff="git diff $BASE_REF_SHA..$PR_REF_SHA"
set +e
files="$($diff --name-only --diff-filter=A -- src/**/*.mli)"
files=$($diff --name-only --diff-filter=A -- src/**/*.mli)
set -e
if [ -n "$files" ]; then
echo '::group::new module(s) added - check index updated too'
Expand All @@ -70,18 +70,18 @@ if [[ $OPAM_DOC -eq 1 ]]; then
fi
fi

htmlfiles=$(ls doc/pages/*.md | sed -e 's/\.md$/.html/')
manfiles=$(opam help topics | sed -e 's|.*|doc/man-html/opam-&.html|')
manfiles="$manfiles $(opam admin help topics | sed -e 's|.*|doc/man-html/opam-admin-&.html|')"
mapfile -t htmlfiles < <(ls doc/pages/*.md | sed -e 's/\.md$/.html/')
mapfile -t manfiles < <(opam help topics | sed -e 's|.*|doc/man-html/opam-&.html|')
mapfile -O "${#manfiles[@]}" -t manfiles < <(opam admin help topics | sed -e 's|.*|doc/man-html/opam-admin-&.html|')

echo '::group::checking for generated files'
echo "pages: $htmlfiles"
echo "topics: $manfiles"
files="$htmlfiles $manfiles"
files=("${htmlfiles[@]}" "${manfiles[@]}")
missing=""
for file in $files; do
if ! test -f $file ; then
missing="$missing $file"
for file in "${files[@]}"; do
if ! test -f "$file" ; then
missing="$missing '$file'"
fi
done
if [ "x$missing" != "x" ]; then
Expand Down

0 comments on commit ca88893

Please sign in to comment.