<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: Times New Roman; font-size: 12pt; color: #000000'>Hi,<div>I am creating a patch for this bug to uncompress examples.</div><div>I will send the patch today or tomorrow</div><div><br></div><div>Olivier</div></div></body></html>