From 90232b0a4c096ed64be34682b16888d5c5d303c6 Mon Sep 17 00:00:00 2001
From: Daku <dakutree@codeanimu.net>
Date: Sat, 31 May 2014 18:20:57 +0100
Subject: [PATCH] rename "index" to "pool index" to help differentiate between
 the two index links

---
 ext/pools/theme.php | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ext/pools/theme.php b/ext/pools/theme.php
index b546d129..fd8bf756 100644
--- a/ext/pools/theme.php
+++ b/ext/pools/theme.php
@@ -138,7 +138,7 @@ class PoolsTheme extends Themelet {
 
 		$nav_html = '<a href="'.make_link().'">Index</a>';
 		$poolnav_html = '
-			<a href="'.make_link("pool/list").'">Index</a>
+			<a href="'.make_link("pool/list").'">Pool Index</a>
 			<br><a href="'.make_link("pool/new").'">Create Pool</a>
 			<br><a href="'.make_link("pool/updated").'">Pool Changes</a>
 		';