/* Executed immediately after outputting the table of contents; ensures
 * that it's shown or hidden as appropriate. */

if (window.showTocToggle)
{
	var tocShowText = "show";
	var tocHideText = "hide";
	showTocToggle();
}