var type = document.location.pathname.match(/\/doc\/html\/spec_html\/filter/) ? 'filter' : 'spec';
// Get the relevant table of contents
var type = document.location.pathname.match(/\/doc\/html\/spec_html\/filter/) ? 'filter' : 'spec';
// Get the relevant table of contents