function insert_version_links() { var labels = ['dev', '0.4', '0.3']; document.write('\n'); }