commit ae90c24fb77d37e02fcfaf0ee9ef64c8b72bb1c1
parent f3c83e3879ec143d00421f2fe5ef75a7067ad1e2
Author: Marcello Stanisci <marcello.stanisci@inria.fr>
Date: Mon, 20 Jun 2016 16:53:09 +0200
addressing #4575
Diffstat:
3 files changed, 22 insertions(+), 0 deletions(-)
diff --git a/Makefile b/Makefile
@@ -53,6 +53,8 @@ clean:
# remove all cached state first.
html:
$(SPHINXBUILD) -b html-linked $(ALLSPHINXOPTS) $(BUILDDIR)/html
+ @cp favicon.ico $(BUILDDIR)/html
+ @cp robots.txt $(BUILDDIR)/html
@echo
@echo "Build finished. The HTML pages are in $(BUILDDIR)/html."
diff --git a/favicon.ico b/favicon.ico
Binary files differ.
diff --git a/robots.txt b/robots.txt
@@ -0,0 +1,20 @@
+#
+# robots.txt
+#
+# This file is to prevent the crawling and indexing of certain parts
+# of your site by web crawlers and spiders run by sites like Yahoo!
+# and Google. By telling these "robots" where not to go on your site,
+# you save bandwidth and server resources.
+#
+# This file will be ignored unless it is at the root of your host:
+# Used: http://example.com/robots.txt
+# Ignored: http://example.com/site/robots.txt
+#
+# For more information about the robots.txt standard, see:
+# http://www.robotstxt.org/robotstxt.html
+#
+# For syntax checking, see:
+# http://www.frobee.com/robots-txt-check
+
+User-agent: *
+Crawl-delay: 10
