You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When building the teaching-guidelines document in multipage HTML
format, numerous multiply-defined labels arise due to apparent
limitations in the GNU Texinfo format, which is used as an
intermediary in the build process. This commit adds a trivial
workaround to prevent this issue from causing the build to fail
due to this issue.
In addition, this commit also fixes some spellchecking failures
for the "definitions" topic.
0 commit comments