(function() {
	document.getElementById('header').innerHTML = generate_file_string();
})();