diff options
| author | Marcello Stanisci <marcello.stanisci@inria.fr> | 2016-06-20 16:53:09 +0200 |
|---|---|---|
| committer | Marcello Stanisci <marcello.stanisci@inria.fr> | 2016-06-20 16:53:09 +0200 |
| commit | ae90c24fb77d37e02fcfaf0ee9ef64c8b72bb1c1 (patch) | |
| tree | a829283f748d4bcccb6e0176ad1fadc546fcd83f | |
| parent | f3c83e3879ec143d00421f2fe5ef75a7067ad1e2 (diff) | |
| download | docs-ae90c24fb77d37e02fcfaf0ee9ef64c8b72bb1c1.tar.gz docs-ae90c24fb77d37e02fcfaf0ee9ef64c8b72bb1c1.tar.bz2 docs-ae90c24fb77d37e02fcfaf0ee9ef64c8b72bb1c1.zip | |
addressing #4575
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | favicon.ico | bin | 0 -> 1150 bytes | |||
| -rw-r--r-- | robots.txt | 20 |
3 files changed, 22 insertions, 0 deletions
@@ -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 differnew file mode 100644 index 00000000..141b93d3 --- /dev/null +++ b/favicon.ico diff --git a/robots.txt b/robots.txt new file mode 100644 index 00000000..0a639917 --- /dev/null +++ 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 |