if( self.location.search == "" ) {	/* no '?file=name' or equivalent present */
	i = self.location.href.lastIndexOf( "/" ) + 1;
	self.location.replace( self.location.href.substring( 0, i ) + "index.php?file=" + self.location.href.substring( i ) ); }