"""
This file provides variables with HTML. It is automatically generated by running bash gen_html.sh.
Do not edit directly.


"""
_="""
"""