improve editor dropdown

dearing / collab

A live code editor using HTML5 technologies

3 stars 1 forks source link

Open dearing opened 11 years ago

dearing commented 11 years ago

The editor dropdown above the current document should include more commonly used tasks, such as changing the theme and language highlighting.

dearing commented 11 years ago

Sadly, using select menus for themes and language highlighting does not fit well in this toolbar.

+1 dropping bootstrap