add robots

Charlie-XIAO · Charlie-XIAO · commit f9e41a38bd69 · 2024-02-03T00:39:01.000+08:00
diff --git a/doc/conf.py b/doc/conf.py
@@ -307,6 +307,10 @@
 # page template can override the one generated from index.rst
 html_additional_pages = {}
 
+# Additional files to copy
+# TODO: remove robots.txt and this entry before merging into main
+html_extra_path = ["robots.txt"]
+
 # Additional JS files
 html_js_files = ["scripts/details-permalink.js"]
 
diff --git a/doc/robots.txt b/doc/robots.txt
@@ -0,0 +1,2 @@
+User-Agent: *
+Disallow: /
