From 27f0f2c9713b2f9a24568cb75733314fa94baa5d Mon Sep 17 00:00:00 2001
From: Shish <shish@shishnet.org>
Date: Wed, 21 Apr 2010 18:03:54 +0100
Subject: [PATCH] link to ext_doc rather than ext_manager, for non-admins

---
 ext/ext_manager/main.php | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/ext/ext_manager/main.php b/ext/ext_manager/main.php
index 11224414..8ee0212b 100644
--- a/ext/ext_manager/main.php
+++ b/ext/ext_manager/main.php
@@ -121,6 +121,9 @@ class ExtManager extends SimpleExtension {
 				$info = new ExtensionInfo("contrib/$ext/main.php");
 				$this->theme->display_doc($page, $info);
 			}
+			else {
+				$this->theme->display_table($page, $this->get_extensions(false), false);
+			}
 		}
 	}
 
@@ -130,7 +133,7 @@ class ExtManager extends SimpleExtension {
 			$event->add_link("Extension Manager", make_link("ext_manager"));
 		}
 		else {
-			$event->add_link("Help", make_link("ext_manager"));
+			$event->add_link("Help", make_link("ext_doc"));
 		}
 	}