Pretty-print warnings as they are created.
This is a debugging aide. Usage is:
ACL2 !> (vl2014::vl-trace-warnings)
This just traces make-vl-warning in a fancy way so that warnings are pretty-printed to the terminal, automatically, whenever they are constructed. This may be useful, along with other debugging output, for figuring out why some warning is being constructed.
This is just a macro based on trace$. You can turn off warning tracing using untrace$.