Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Fix history deletion bug after font size change #7668
Hmm... when I had implemented this, I encountered that the font size change only works after clearing the console (because of some html subsystem). The console content should be restored at L494.
Are you sure the console window gets cleared when changing the font size? If so, what platform?