Why do:<div><span class="Apple-style-span" style="font-family: Times; font-size: medium; -webkit-border-horizontal-spacing: 2px; -webkit-border-vertical-spacing: 2px; "><u style="text-decoration: none;"><b style=""><ul style="text-decoration: underline;">

<li>PETSC_VIEWER_XXXX is now PETSCVIEWERXXX</li></ul><div><span class="Apple-style-span" style="font-size: small;"><span class="Apple-style-span" style="font-weight: normal;"><>Srinath</span></span></div></b></u></span></div>