mn200/HOL — Issue #42: HOL munger should not translate inside LaTeX comments
Author: mn200
Created: 2011-11-02 00:46:19+00:00
State: open
Labels: Feature Request

The built-in lexer should know when it has just passed over a %... On the other hand, having to spot that it's inside a verbatim type environment is a very hard prospect.