Oops sorry, I forgot to add that I have no strong opinion on the type (I only have a minor preference for str only).<div><br></div><div>Victor</div>