diff --git a/ci/dox.sh b/ci/dox.sh index bcf20de5bfc29..4fe0dc5dad8df 100644 --- a/ci/dox.sh +++ b/ci/dox.sh @@ -60,7 +60,7 @@ while read -r target; do mkdir -p "${TARGET_DOC_DIR}/${target}" cp -r "target/${target}/doc" "${TARGET_DOC_DIR}/${target}" - echo "* [${target}](${target}/libc/index.html)" >> $PLATFORM_SUPPORT + echo "* [${target}](${target}/doc/libc/index.html)" >> $PLATFORM_SUPPORT done < targets # Replace
with the contents of $PLATFORM_SUPPORT