sent from a phone > On 24. Aug 2020, at 22:10, Joseph Eisenberg <joseph.eisenberg at gmail.com> wrote: > > But if you want to change the definition how could you change the definition of an undocumented tag? Cheers Martin