2 const MenuButton = document.getElementById("menu_button");
5 const Menu = document.getElementById("menu");
8 const ReleaseIdForm = document.getElementById("releaseidform");
11 const EditionForm = document.getElementById("editionform");
14 const DownloadButton = document.getElementById("downloadbutton");
17 const Main = document.getElementById("main");
20 const MetaTitle = document.getElementById("meta_title");
23 const HeaderTitle = document.getElementById("header_title");