Index: vhosts/server.php
===================================================================
--- vhosts/server.php	(revision 292)
+++ vhosts/server.php	(revision 293)
@@ -4,4 +4,10 @@
 if (isset($_SERVER['PATH_INFO'])) $pi = explode('/',$_SERVER['PATH_INFO']);
 if (isset($_SERVER['SERVER_PORT'])) $port = $_SERVER['SERVER_PORT']; else $port = '80';
+
+if ($req == '/robots.txt') {
+	header('Content-Type: text/plain');
+	fpassthru('/afs/athena.mit.edu/contrib/scripts/web_scripts/robots.txt');
+	exit;
+}
 
 if (array_shift(explode('.',$name)) == 'www') {