Thanks for the bug report; that is fixed in CVS now.

Reply via email to