diff options
Diffstat (limited to 'html')
| -rw-r--r-- | html/eproofe | 5 | ||||
| -rw-r--r-- | html/robots.txt | 6 |
2 files changed, 11 insertions, 0 deletions
diff --git a/html/eproofe b/html/eproofe new file mode 100644 index 00000000..4965773a --- /dev/null +++ b/html/eproofe @@ -0,0 +1,5 @@ +<?php include('eeproof.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?> diff --git a/html/robots.txt b/html/robots.txt new file mode 100644 index 00000000..855ec318 --- /dev/null +++ b/html/robots.txt @@ -0,0 +1,6 @@ +# robots.txt for http://proofgeneral.inf.ed.ac.uk +# see http://httpd.apache.org/docs/misc/howto.html + +User-agent: * +Disallow: /cgi/ # cgi scripts +# Disallow: /manual/ # get it somewhere else |