diff --git a/tools/build-rst.sh b/tools/build-rst.sh index 5861ccc0ea..e102b15567 100755 --- a/tools/build-rst.sh +++ b/tools/build-rst.sh @@ -105,5 +105,7 @@ else if [ "$TARGET" != "" ] ; then mkdir -p publish-docs/$TARGET rsync -a $BUILD_DIR/ publish-docs/$TARGET/ + # Remove unneeded build artefact + rm -f publish-docs/$TARGET/.buildinfo fi fi