From 01c082065a6c496baf9bae664520a4ed706277d8 Mon Sep 17 00:00:00 2001
From: Jimmy Collins <collinj@users.mediawiki.org>
Date: Tue, 19 Sep 2006 12:23:56 +0000
Subject: [PATCH] stub

---
 config/index.php | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/config/index.php b/config/index.php
index 1d75eab870..90e36c2aa6 100644
--- a/config/index.php
+++ b/config/index.php
@@ -1225,7 +1225,7 @@ which means that anyone on the same server can read your database password! Down
 it and uploading it again will hopefully change the ownership to a user ID specific to you.</p>
 EOT;
 	} else {
-		echo "<p><span style='font-weight:bold;color:green;font-size:110%'>Installation successful!</span> Move the config/LocalSettings.php file into the parent directory, then follow
+		echo "<p><span style='font-weight:bold;color:green;font-size:110%'>Installation successful!</span> Move the <tt>config/LocalSettings.php</tt> file into the parent directory, then follow
 			<strong><a href='../index.php'>this link</a></strong> to your wiki.</p>\n";
 	}
 }
-- 
2.20.1