gh-38694: Add robots.txt file to doc preview websites for PRs and releases
    
<!-- ^ Please provide a concise and informative title. -->
<!-- ^ Don't put issue numbers in the title, do this in the PR
description below. -->
<!-- ^ For example, instead of "Fixes #12345" use "Introduce new method
to calculate 1 + 2". -->
<!-- v Describe your changes below in detail. -->
<!-- v Why is this change required? What problem does it solve? -->
<!-- v If this PR resolves an open issue, please link to it here. For
example, "Fixes #12345". -->

We are experiencing an extraordinary surge of access to the doc preview
websites for PRs and releases.
<img width="924" alt="Screenshot 2024-09-22 at 2 24 56 PM"
src="https://github.com/user-
attachments/assets/e7d49ae9-b14e-485f-95bf-3dee2d4f3bc6">
We suspect that it is by web crawlers indexing the websites. This may be
a good thing for our doc sites for stable releases, but a threat of
excessive use of limited bandwidth (100GB monthly) of our netlify (web
publishing service) resource.

Hence we add "robots.txt" file to the websites to discourage web
crawlers.

### 📝 Checklist

<!-- Put an `x` in all the boxes that apply. -->

- [x] The title is concise and informative.
- [x] The description explains in detail what this PR is about.
- [ ] I have linked a relevant issue or discussion.
- [ ] I have created tests covering the changes.
- [ ] I have updated the documentation and checked the documentation
preview.

### ⌛ Dependencies

<!-- List all open PRs that this PR logically depends on. For example,
-->
<!-- - #12345: short description why this is a dependency -->
<!-- - #34567: ... -->
    
URL: #38694
Reported by: Kwankyu Lee
Reviewer(s): Frédéric Chapoton

Author: Release Manager

.github/workflows/doc-build.yml

@@ -213,6 +213,9 @@ jobs:
             (cd doc && mv .git ../git && mv .gitattributes ../gitattributes)
             mv CHANGES.html doc
           fi
+          # Create the robots.txt file to discourage web crawlers from indexing doc preview webpages
+          echo "User-agent: *" > doc/robots.txt
+          echo "Disallow: /" >> doc/robots.txt
           # Zip everything for increased performance
           zip -r doc.zip doc