[CHANGE] Reserved labels
6 views
Skip to first unread message
Rob Beezer
Jun 30, 2026, 2:04:17 PM (4 days ago) Jun 30
to pretext-...@googlegroups.com
We need to reserve some identifiers for smooth functioning of the HTML version
of your projects. To this end, we are reserving any string that begins with "ptx-".
So a @label, or no @label and an @xml:id, which begins this way, will cause a
fatal error. The fix is to simply make an edit.
Hopefully this will not be too much trouble for anybody.
Rob
of your projects. To this end, we are reserving any string that begins with "ptx-".
So a @label, or no @label and an @xml:id, which begins this way, will cause a
fatal error. The fix is to simply make an edit.
Hopefully this will not be too much trouble for anybody.
Rob
Reply all
Reply to author
Forward
0 new messages