text: // Miscellaneous enhancements to doc display
  
  
  $(document).ready(function() {
  	/*** Add permalink buttons next to glossary terms ***/
  
  	$('dl.glossary > dt[id]').append(function() {
  		return ('<a class="headerlink" href="#' +
  			    this.getAttribute('id') +
  			    '" title="Permalink to this term">¶</a>');
  	})
  });
  