function display_user_menu()
{
- global $wiki,$myid,$INDEX,$STATS;
+ global $WIKI,$myid,$INDEX,$STATS;
echo "<div class=\"usermenu\">\n".
"<a href=\"".$INDEX."\"> Go to my user page </a>";
echo "<hr /> <a href=\"".$STATS."\">Statistics</a>\n";
echo
- "<hr />Report bugs in the <a href=\"".$wiki."\">wiki</a>\n";
+ "<hr />Report bugs in the <a href=\"".$WIKI."\">wiki</a>\n";
echo "</div>\n";
return;
}