What are these comments for in Happy ?<div><br></div><div>    {-# SCC &quot;Mangler&quot; #-}</div><div><br></div><div>Many thanks in advance,</div><div><br></div><div>Aaron</div><div><br></div>