From bfb731e06524605a094e8e6708fc6b307d8b3a9d Mon Sep 17 00:00:00 2001
From: Eli Barzilay <eli@barzilay.org>
Date: Mon, 20 Feb 2012 05:27:29 -0500
Subject: [PATCH] Add robots.txt, to avoid spiders hammering the server via
 gitweb.

---
 collects/meta/web/stubs/git.rkt | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/collects/meta/web/stubs/git.rkt b/collects/meta/web/stubs/git.rkt
index 8a3b5a5899..f60de001b7 100644
--- a/collects/meta/web/stubs/git.rkt
+++ b/collects/meta/web/stubs/git.rkt
@@ -27,6 +27,11 @@
     @p{See the "brief", PLT-oriented @intro{introduction to git}.}}))
 (define home-file @plain[#:file "home-text.html" home-text])
 
+(define robots.txt
+  @plain{User-agent: *
+         @(add-newlines (for/list ([d '(plt libs testing play)])
+                          @list{Disallow: /@|d|/}))})
+
 (define gitweb-config
   @plain[#:file "gitweb_config.perl"]{
     our $projectroot = "repos";