-
Notifications
You must be signed in to change notification settings - Fork 772
Possible CI check: bad use of \grammarterm #1543
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Comments
Update: Recent commits fixed a lot of bad uses! The list now is:
|
Update: Capitalized \grammarterms are also considered bad, see #1519. Removing the
|
Recent commits fixed many bad uses, reducing the list to:
We're nearly there! :) |
Update: by now the list has been reduced to:
|
dot and dot-dot are addressed by #1527. |
In my last update, I forgot to include the capitalized grammarterms that are also considered bad (#1519). These also still exist:
|
#1858 fixed the last remnants of these. |
Uh oh!
There was an error while loading. Please reload this page.
It's pretty easy to get lists of uses of \grammarterm and \nontermdef, and to compare them:
This finds the following uses of \grammarterm that don't have a corresponding \nontermdef:
I think at most a couple of these are ok, all the rest are bad as far as I can tell.
So maybe this could be a Travis check, possibly with a short whitelist. I suppose all current bad uses would have to be fixed first though. Thoughts?
The text was updated successfully, but these errors were encountered: