Join GitHub today
GitHub is home to over 40 million developers working together to host and review code, manage projects, and build software together.Sign up
Hide 'Export as HTML' submenu #53
Moreover, the HTML export doesn't work fine ATM and I'm not sure it's worth spending time fixing it since it's not easy (@arcilli already spent some time investigating) and I don't think this feature is used that much. Of course, we can later re-evaluate this in case we'll see requests for this feature.