The mail server just told me that the commit that removes the symbols files is too large (~2MB). I don't intend to force the mail in, it carries little value and would only clutter the mail archives for eternity. Thomas