search

oscarlevin / pretext-tools

MIT License
7 stars 9 forks source link

Comment selection #55

Closed JCBustamante closed 1 year ago

JCBustamante commented 1 year ago

Would be nice if one could comment / uncomment a text selection, that is insert < ! - - xxx - - >

oscarlevin commented 1 year ago

Does the shortcut ctrl+/ (or cmd+/ if on Mac) do what you want?